# Compact sets in uniform spaces #

- `compactSpace_uniformity`: On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.

source
theorem lebesgue_number_lemma {α : Type ua} [UniformSpace α] {K : Set α} {ι : Sort u_2} {U : ι → Set α} (hK : IsCompact K) (hopen : ∀ (i : ι), IsOpen (U i)) (hcover : K ⊆ ⋃ (i : ι), U i) :
∃ V ∈ uniformity α, ∀ x ∈ K, ∃ (i : ι), UniformSpace.ball x V ⊆ U i

Let `c : ι → Set α` be an open cover of a compact set `s`. Then there exists an entourage `n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `c i`.

source
theorem lebesgue_number_lemma_nhds' {α : Type ua} [UniformSpace α] {K : Set α} {U : (x : α) → x ∈ K → Set α} (hK : IsCompact K) (hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ nhds x) :
∃ V ∈ uniformity α, ∀ x ∈ K, ∃ (y : ↑K), UniformSpace.ball x V ⊆ U ↑y ⋯
source
theorem lebesgue_number_lemma_nhds {α : Type ua} [UniformSpace α] {K : Set α} {U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ nhds x) :
∃ V ∈ uniformity α, ∀ x ∈ K, ∃ (y : α), UniformSpace.ball x V ⊆ U y
source
theorem lebesgue_number_lemma_nhdsWithin' {α : Type ua} [UniformSpace α] {K : Set α} {U : (x : α) → x ∈ K → Set α} (hK : IsCompact K) (hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ nhdsWithin x K) :
∃ V ∈ uniformity α, ∀ x ∈ K, ∃ (y : ↑K), UniformSpace.ball x V ∩ K ⊆ U ↑y ⋯
source
theorem lebesgue_number_lemma_nhdsWithin {α : Type ua} [UniformSpace α] {K : Set α} {U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ nhdsWithin x K) :
∃ V ∈ uniformity α, ∀ x ∈ K, ∃ (y : α), UniformSpace.ball x V ∩ K ⊆ U y
source
theorem Filter.HasBasis.lebesgue_number_lemma {α : Type ua} [UniformSpace α] {K : Set α} {ι' : Sort u_2} {ι : Sort u_3} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : ι → Set α} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) (hopen : ∀ (j : ι), IsOpen (U j)) (hcover : K ⊆ ⋃ (j : ι), U j) :
∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (j : ι), UniformSpace.ball x (V i) ⊆ U j

Let `U : ι → Set α` be an open cover of a compact set `K`. Then there exists an entourage `V` such that for each `x ∈ K` its `V`-neighborhood is included in some `U i`.

Moreover, one can choose an entourage from a given basis.

source
theorem Filter.HasBasis.lebesgue_number_lemma_nhds' {α : Type ua} [UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : (x : α) → x ∈ K → Set α} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) (hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ nhds x) :
∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : ↑K), UniformSpace.ball x (V i) ⊆ U ↑y ⋯
source
theorem Filter.HasBasis.lebesgue_number_lemma_nhds {α : Type ua} [UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : α → Set α} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ nhds x) :
∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : α), UniformSpace.ball x (V i) ⊆ U y
source
theorem Filter.HasBasis.lebesgue_number_lemma_nhdsWithin' {α : Type ua} [UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : (x : α) → x ∈ K → Set α} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) (hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ nhdsWithin x K) :
∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : ↑K), UniformSpace.ball x (V i) ∩ K ⊆ U ↑y ⋯
source
theorem Filter.HasBasis.lebesgue_number_lemma_nhdsWithin {α : Type ua} [UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : α → Set α} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ nhdsWithin x K) :
∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : α), UniformSpace.ball x (V i) ∩ K ⊆ U y
source
theorem lebesgue_number_lemma_sUnion {α : Type ua} [UniformSpace α] {K : Set α} {S : Set (Set α)} (hK : IsCompact K) (hopen : ∀ s ∈ S, IsOpen s) (hcover : K ⊆ ⋃₀ S) :
∃ V ∈ uniformity α, ∀ x ∈ K, ∃ s ∈ S, UniformSpace.ball x V ⊆ s

Let `c : Set (Set α)` be an open cover of a compact set `s`. Then there exists an entourage `n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `t ∈ c`.

source
theorem IsCompact.nhdsSet_basis_uniformity {α : Type ua} {ι : Sort u_1} [UniformSpace α] {K : Set α} {p : ι → Prop} {V : ι → Set (α × α)} (hbasis : (uniformity α).HasBasis p V) (hK : IsCompact K) :
(nhdsSet K).HasBasis p fun (i : ι) => ⋃ x ∈ K, UniformSpace.ball x (V i)

If `K` is a compact set in a uniform space and `{V i | p i}` is a basis of entourages, then `{⋃ x ∈ K, UniformSpace.ball x (V i) | p i}` is a basis of `𝓝ˢ K`.

Here "`{s i | p i}` is a basis of a filter `l`" means `Filter.HasBasis l p s`.

source
theorem Disjoint.exists_uniform_thickening {α : Type ua} [UniformSpace α] {A B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) :
∃ V ∈ uniformity α, Disjoint (⋃ x ∈ A, UniformSpace.ball x V) (⋃ x ∈ B, UniformSpace.ball x V)
source
theorem Disjoint.exists_uniform_thickening_of_basis {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)} (hU : (uniformity α).HasBasis p s) {A B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) :
∃ (i : ι), p i ∧ Disjoint (⋃ x ∈ A, UniformSpace.ball x (s i)) (⋃ x ∈ B, UniformSpace.ball x (s i))
source
theorem lebesgue_number_of_compact_open {α : Type ua} [UniformSpace α] {K U : Set α} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
∃ V ∈ uniformity α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U

A useful consequence of the Lebesgue number lemma: given any compact set `K` contained in an open set `U`, we can find an (open) entourage `V` such that the ball of size `V` about any point of `K` is contained in `U`.

source
theorem nhdsSet_diagonal_eq_uniformity {α : Type ua} [UniformSpace α] [CompactSpace α] :
nhdsSet (Set.diagonal α) = uniformity α

On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.

source
theorem compactSpace_uniformity {α : Type ua} [UniformSpace α] [CompactSpace α] :
uniformity α = ⨆ (x : α), nhds (x, x)

On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.

source
theorem unique_uniformity_of_compact {γ : Type uc} [t : TopologicalSpace γ] [CompactSpace γ] {u u' : UniformSpace γ} (h : u.toTopologicalSpace = t) (h' : u'.toTopologicalSpace = t) :
u = u'