Covers in a uniform space

This file defines covers, aka nets, which are a quantitative notion of compactness given an entourage.

A U-cover of a set s is a set N such that every element of s is U-close to some element of N.

The concept of uniform covers can be used to define two further notions of covering:

• Metric covers: Metric.IsCover, defined using the distance entourage.
• Dynamical covers: Dynamics.IsDynCoverOf, defined using the dynamical entourage.

References

[R. Vershynin, High Dimensional Probability][vershynin2018high], Section 4.2.

def SetRel.IsCover {X : Type u_1} (U : SetRel X X) (s N : Set X) : Prop

For an entourage U, a set N is a U-cover of a set s if every point of s is U-close to some point of N.

This is also called a U-net in the literature.

[R. Vershynin, High Dimensional Probability][vershynin2018high], 4.2.1.

Equations

• U.IsCover s N = ∀ ⦃x : X⦄, x ∈ s → ∃ y ∈ N, (x, y) ∈ U

@[simp]

theorem SetRel.IsCover.empty {X : Type u_1} {U : SetRel X X} {N : Set X} : U.IsCover ∅ N

@[simp]

theorem SetRel.isCover_empty_right {X : Type u_1} {U : SetRel X X} {s : Set X} : U.IsCover s ∅ ↔ s = ∅

theorem SetRel.IsCover.nonempty {X : Type u_1} {U : SetRel X X} {s N : Set X} (hsN : U.IsCover s N) (hs : s.Nonempty) : N.Nonempty

@[simp]

theorem SetRel.IsCover.refl {X : Type u_1} (U : SetRel X X) [U.IsRefl] (s : Set X) : U.IsCover s s

theorem SetRel.IsCover.rfl {X : Type u_1} {U : SetRel X X} [U.IsRefl] {s : Set X} : U.IsCover s s

@[simp]

theorem SetRel.isCover_univ {X : Type u_1} {s N : Set X} : IsCover Set.univ s N ↔ s.Nonempty → N.Nonempty

theorem SetRel.IsCover.mono {X : Type u_1} {U : SetRel X X} {s N₁ N₂ : Set X} (hN : N₁ ⊆ N₂) (h₁ : U.IsCover s N₁) : U.IsCover s N₂

theorem SetRel.IsCover.anti {X : Type u_1} {U : SetRel X X} {s t N : Set X} (hst : s ⊆ t) (ht : U.IsCover t N) : U.IsCover s N

theorem SetRel.IsCover.mono_entourage {X : Type u_1} {U V : SetRel X X} {s N : Set X} (hUV : U ⊆ V) (hU : U.IsCover s N) : V.IsCover s N

theorem SetRel.IsCover.of_maximal_isSeparated {X : Type u_1} {U : SetRel X X} {s N : Set X} [U.IsRefl] [U.IsSymm] (hN : Maximal (fun (N : Set X) => N ⊆ s ∧ U.IsSeparated N) N) : U.IsCover s N

A maximal U-separated subset of a set s is a U-cover of s.

[R. Vershynin, High Dimensional Probability][vershynin2018high], 4.2.6.

@[simp]

theorem SetRel.isCover_relId {X : Type u_1} {s N : Set X} : SetRel.id.IsCover s N ↔ s ⊆ N