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.

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.

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 ⋯

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

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 ⋯

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

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.

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 ⋯

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

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 ⋯

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

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.

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.

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)

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))

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.

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.

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.

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

theorem IsClosed.relPreimage_of_isCompact {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsClosed s) {t : Set β} (ht : IsCompact t) : IsClosed (s.preimage t)

theorem IsClosed.relImage_of_isCompact {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsClosed s) {t : Set α} (ht : IsCompact t) : IsClosed (s.image t)