doc-next-gen

Mathlib.Topology.UniformSpace.Compact

Module docstring

{"# 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.

"}

lebesgue_number_lemma theorem
{ι : Sort*} {U : ι → Set α} (hK : IsCompact K) (hopen : ∀ i, IsOpen (U i)) (hcover : K ⊆ ⋃ i, U i) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i
Full source 
/-- 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 {ι : Sort*} {U : ι → Set α} (hK : IsCompact K)
    (hopen : ∀ i, IsOpen (U i)) (hcover : K ⊆ ⋃ i, U i) :
    ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ i, ball x V ⊆ U i := by
  have : ∀ x ∈ K, ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i := fun x hx ↦ by
    obtain ⟨i, hi⟩ := mem_iUnion.1 (hcover hx)
    rw [← (hopen i).mem_nhds_iff, nhds_eq_comap_uniformity, ← lift'_comp_uniformity] at hi
    exact ⟨i, (((basis_sets _).lift' <| monotone_id.compRel monotone_id).comap _).mem_iff.1 hi⟩
  choose ind W hW hWU using this
  rcases hK.elim_nhds_subcover' (fun x hx ↦ ball x (W x hx)) (fun x hx ↦ ball_mem_nhds _ (hW x hx))
    with ⟨t, ht⟩
  refine ⟨⋂ x ∈ t, W x x.2, (biInter_finset_mem _).2 fun x _ ↦ hW x x.2, fun x hx ↦ ?_⟩
  rcases mem_iUnion₂.1 (ht hx) with ⟨y, hyt, hxy⟩
  exact ⟨ind y y.2, fun z hz ↦ hWU _ _ ⟨x, hxy, mem_iInter₂.1 hz _ hyt⟩⟩
Lebesgue Number Lemma for Uniform Spaces
Informal description
Let $K$ be a compact subset of a uniform space $\alpha$, and let $\{U_i\}_{i \in \iota}$ be an open cover of $K$. Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is entirely contained in some $U_i$.
lebesgue_number_lemma_nhds' theorem
{U : (x : α) → x ∈ K → Set α} (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ⊆ U y y.2
Full source 
theorem lebesgue_number_lemma_nhds' {U : (x : α) → x ∈ K → Set α} (hK : IsCompact K)
    (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ⊆ U y y.2 := by
  rcases lebesgue_number_lemma (U := fun x : K => interior (U x x.2)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩
  exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩
Lebesgue Number Lemma for Neighborhoods in Uniform Spaces
Informal description
Let $K$ be a compact subset of a uniform space $\alpha$, and for each $x \in K$, let $U_x$ be a neighborhood of $x$ in $\alpha$. Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, there exists $y \in K$ with the uniform ball $\{z \in \alpha \mid (x, z) \in V\}$ entirely contained in $U_y$.
lebesgue_number_lemma_nhds theorem
{U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝 x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y
Full source 
theorem lebesgue_number_lemma_nhds {U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝 x) :
    ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U y := by
  rcases lebesgue_number_lemma (U := fun x => interior (U x)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩
  exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩
Lebesgue Number Lemma for Neighborhoods in Uniform Spaces
Informal description
Let $K$ be a compact subset of a uniform space $\alpha$, and for each $x \in K$, let $U(x)$ be a neighborhood of $x$. Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, there exists a point $y$ with the uniform ball $\{z \in \alpha \mid (x, z) \in V\}$ entirely contained in $U(y)$.
lebesgue_number_lemma_nhdsWithin' theorem
{U : (x : α) → x ∈ K → Set α} (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝[K] x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ∩ K ⊆ U y y.2
Full source 
theorem lebesgue_number_lemma_nhdsWithin' {U : (x : α) → x ∈ K → Set α} (hK : IsCompact K)
    (hU : ∀ x hx, U x hx ∈ 𝓝[K] x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y : K, ball x V ∩ K ⊆ U y y.2 :=
  (lebesgue_number_lemma_nhds' hK (fun x hx => Filter.mem_inf_principal'.1 (hU x hx))).imp
    fun _ ⟨V_uni, hV⟩ => ⟨V_uni, fun x hx => (hV x hx).imp fun _ hy => (inter_subset _ _ _).2 hy⟩
Lebesgue Number Lemma for Relative Neighborhoods in Compact Subsets of Uniform Spaces
Informal description
Let $K$ be a compact subset of a uniform space $\alpha$, and for each $x \in K$, let $U_x$ be a neighborhood of $x$ relative to $K$ (i.e., $U_x \in \mathcal{N}_K(x)$, the neighborhood filter of $x$ in the subspace topology on $K$). Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, there exists $y \in K$ with the intersection of the uniform ball $\{z \in \alpha \mid (x, z) \in V\}$ with $K$ entirely contained in $U_y$.
lebesgue_number_lemma_nhdsWithin theorem
{U : α → Set α} (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝[K] x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ∩ K ⊆ U y
Full source 
theorem lebesgue_number_lemma_nhdsWithin {U : α → Set α} (hK : IsCompact K)
    (hU : ∀ x ∈ K, U x ∈ 𝓝[K] x) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ∩ K ⊆ U y :=
  (lebesgue_number_lemma_nhds hK (fun x hx => Filter.mem_inf_principal'.1 (hU x hx))).imp
    fun _ ⟨V_uni, hV⟩ => ⟨V_uni, fun x hx => (hV x hx).imp fun _ hy => (inter_subset _ _ _).2 hy⟩
Lebesgue Number Lemma for Relative Neighborhoods in Compact Uniform Spaces
Informal description
Let $K$ be a compact subset of a uniform space $\alpha$, and for each $x \in K$, let $U(x)$ be a neighborhood of $x$ relative to $K$ (i.e., $U(x) \in \mathcal{N}_K(x)$). Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, there exists a point $y$ with the intersection of the uniform ball $\{z \in \alpha \mid (x, z) \in V\}$ and $K$ entirely contained in $U(y)$.
Filter.HasBasis.lebesgue_number_lemma theorem
{ι' ι : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : ι → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hopen : ∀ j, IsOpen (U j)) (hcover : K ⊆ ⋃ j, U j) : ∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j
Full source 
/-- 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. -/
protected theorem Filter.HasBasis.lebesgue_number_lemma {ι' ι : Sort*} {p : ι' → Prop}
    {V : ι' → Set (α × α)} {U : ι → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K)
    (hopen : ∀ j, IsOpen (U j)) (hcover : K ⊆ ⋃ j, U j) :
    ∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j := by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)
  exact fun s t hst ht x hx ↦ (ht x hx).imp fun i hi ↦ Subset.trans (ball_mono hst _) hi
Lebesgue Number Lemma for Uniform Spaces with Basis
Informal description
Let $\alpha$ be a uniform space with a basis $\{V_i\}_{i \in \iota'}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. Let $K$ be a compact subset of $\alpha$, and let $\{U_j\}_{j \in \iota}$ be an open cover of $K$. Then there exists an index $i$ such that $p(i)$ holds and for every $x \in K$, there exists some $j$ such that the uniform ball $\{y \in \alpha \mid (x, y) \in V_i\}$ is entirely contained in $U_j$.
Filter.HasBasis.lebesgue_number_lemma_nhds' theorem
{ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : (x : α) → x ∈ K → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ i, p i ∧ ∀ x ∈ K, ∃ y : K, ball x (V i) ⊆ U y y.2
Full source 
protected theorem Filter.HasBasis.lebesgue_number_lemma_nhds' {ι' : Sort*} {p : ι' → Prop}
    {V : ι' → Set (α × α)} {U : (x : α) → x ∈ K → Set α} (hbasis : (𝓤 α).HasBasis p V)
    (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝 x) :
    ∃ i, p i ∧ ∀ x ∈ K, ∃ y : K, ball x (V i) ⊆ U y y.2 := by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds' hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy
Lebesgue Number Lemma for Uniform Spaces with Basis and Pointwise Neighborhoods
Informal description
Let $\alpha$ be a uniform space with a basis $\{V_i\}_{i \in \iota'}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. Let $K$ be a compact subset of $\alpha$, and for each $x \in K$, let $U_x$ be a neighborhood of $x$ in $\alpha$. Then there exists an index $i$ such that $p(i)$ holds and for every $x \in K$, there exists $y \in K$ with the uniform ball $\{z \in \alpha \mid (x, z) \in V_i\}$ entirely contained in $U_y$.
Filter.HasBasis.lebesgue_number_lemma_nhds theorem
{ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : α → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝 x) : ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ⊆ U y
Full source 
protected theorem Filter.HasBasis.lebesgue_number_lemma_nhds {ι' : Sort*} {p : ι' → Prop}
    {V : ι' → Set (α × α)} {U : α → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K)
    (hU : ∀ x ∈ K, U x ∈ 𝓝 x) : ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ⊆ U y := by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy
Lebesgue Number Lemma for Uniform Spaces with Basis and Neighborhoods
Informal description
Let $\alpha$ be a uniform space with a basis $\{V_i\}_{i \in \iota'}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. Let $K$ be a compact subset of $\alpha$, and for each $x \in K$, let $U(x)$ be a neighborhood of $x$. Then there exists an index $i$ such that $p(i)$ holds and for every $x \in K$, there exists a point $y$ such that the uniform ball $\{z \in \alpha \mid (x, z) \in V_i\}$ is entirely contained in $U(y)$.
Filter.HasBasis.lebesgue_number_lemma_nhdsWithin' theorem
{ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : (x : α) → x ∈ K → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝[K] x) : ∃ i, p i ∧ ∀ x ∈ K, ∃ y : K, ball x (V i) ∩ K ⊆ U y y.2
Full source 
protected theorem Filter.HasBasis.lebesgue_number_lemma_nhdsWithin' {ι' : Sort*} {p : ι' → Prop}
    {V : ι' → Set (α × α)} {U : (x : α) → x ∈ K → Set α} (hbasis : (𝓤 α).HasBasis p V)
    (hK : IsCompact K) (hU : ∀ x hx, U x hx ∈ 𝓝[K] x) :
    ∃ i, p i ∧ ∀ x ∈ K, ∃ y : K, ball x (V i) ∩ K ⊆ U y y.2 := by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin' hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy
Lebesgue Number Lemma for Uniform Spaces with Basis and Relative Neighborhoods
Informal description
Let $\alpha$ be a uniform space with a basis $\{V_i\}_{i \in \iota'}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. Let $K$ be a compact subset of $\alpha$, and for each $x \in K$, let $U_x$ be a neighborhood of $x$ relative to $K$. Then there exists an index $i$ such that $p(i)$ holds and for every $x \in K$, there exists $y \in K$ such that the intersection of the uniform ball $\{z \in \alpha \mid (x, z) \in V_i\}$ with $K$ is contained in $U_y$.
Filter.HasBasis.lebesgue_number_lemma_nhdsWithin theorem
{ι' : Sort*} {p : ι' → Prop} {V : ι' → Set (α × α)} {U : α → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) (hU : ∀ x ∈ K, U x ∈ 𝓝[K] x) : ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ∩ K ⊆ U y
Full source 
protected theorem Filter.HasBasis.lebesgue_number_lemma_nhdsWithin {ι' : Sort*} {p : ι' → Prop}
    {V : ι' → Set (α × α)} {U : α → Set α} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K)
    (hU : ∀ x ∈ K, U x ∈ 𝓝[K] x) : ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ∩ K ⊆ U y := by
  refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy
Lebesgue Number Lemma for Relative Neighborhoods in Compact Uniform Spaces with Basis
Informal description
Let $\alpha$ be a uniform space with a basis $\{V_i\}_{i \in \iota'}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. Let $K$ be a compact subset of $\alpha$, and for each $x \in K$, let $U(x)$ be a neighborhood of $x$ relative to $K$. Then there exists an index $i$ such that $p(i)$ holds and for every $x \in K$, there exists a point $y$ such that the intersection of the uniform ball $\{z \in \alpha \mid (x, z) \in V_i\}$ with $K$ is entirely contained in $U(y)$.
lebesgue_number_lemma_sUnion theorem
{S : Set (Set α)} (hK : IsCompact K) (hopen : ∀ s ∈ S, IsOpen s) (hcover : K ⊆ ⋃₀ S) : ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s
Full source 
/-- 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 lebesgue_number_lemma_sUnion {S : Set (Set α)}
    (hK : IsCompact K) (hopen : ∀ s ∈ S, IsOpen s) (hcover : K ⊆ ⋃₀ S) :
    ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s := by
  rw [sUnion_eq_iUnion] at hcover
  simpa using lebesgue_number_lemma hK (by simpa) hcover
Lebesgue Number Lemma for Open Covers in Uniform Spaces
Informal description
Let $K$ be a compact subset of a uniform space $\alpha$, and let $S$ be a collection of open subsets of $\alpha$ such that $K \subseteq \bigcup_{s \in S} s$. Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, there exists a set $s \in S$ for which the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is entirely contained in $s$.
IsCompact.nhdsSet_basis_uniformity theorem
{p : ι → Prop} {V : ι → Set (α × α)} (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) : (𝓝ˢ K).HasBasis p fun i => ⋃ x ∈ K, ball x (V i)
Full source 
/-- 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 IsCompact.nhdsSet_basis_uniformity {p : ι → Prop} {V : ι → Set (α × α)}
    (hbasis : (𝓤 α).HasBasis p V) (hK : IsCompact K) :
    (𝓝ˢ K).HasBasis p fun i => ⋃ x ∈ K, ball x (V i) where
  mem_iff' U := by
    constructor
    · intro H
      have HKU : K ⊆ ⋃ _ : Unit, interior U := by
        simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
      obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU
      exact ⟨i, hpi, hi.trans interior_subset⟩
    · rintro ⟨i, hpi, hi⟩
      refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi
      exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi
Basis of Neighborhoods for Compact Sets in Uniform Spaces
Informal description
Let $\alpha$ be a uniform space with a basis $\{V_i\}_{i \in \iota}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. For any compact subset $K \subseteq \alpha$, the neighborhood filter $\mathcal{N}^s(K)$ of $K$ has a basis consisting of sets of the form $\bigcup_{x \in K} \{y \in \alpha \mid (x, y) \in V_i\}$, where $i$ ranges over indices satisfying $p(i)$.
Disjoint.exists_uniform_thickening theorem
{A B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) : ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
Full source 
theorem Disjoint.exists_uniform_thickening {A B : Set α} (hA : IsCompact A) (hB : IsClosed B)
    (h : Disjoint A B) : ∃ V ∈ 𝓤 α, Disjoint (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V) := by
  have : BᶜBᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
  rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this
  rcases this with ⟨U, hU, hUAB⟩
  rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
  refine ⟨V, hV, Set.disjoint_left.mpr fun x => ?_⟩
  simp only [mem_iUnion₂]
  rintro ⟨a, ha, hxa⟩ ⟨b, hb, hxb⟩
  rw [mem_ball_symmetry hVsymm] at hxa hxb
  exact hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hVsymm hxa hxb) hb
Existence of Uniform Thickening for Disjoint Compact and Closed Sets
Informal description
Let $A$ and $B$ be subsets of a uniform space $\alpha$ such that $A$ is compact, $B$ is closed, and $A$ and $B$ are disjoint. Then there exists an entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that the uniform thickenings $\bigcup_{x \in A} \{y \in \alpha \mid (x, y) \in V\}$ and $\bigcup_{x \in B} \{y \in \alpha \mid (x, y) \in V\}$ are disjoint.
Disjoint.exists_uniform_thickening_of_basis theorem
{p : ι → Prop} {s : ι → Set (α × α)} (hU : (𝓤 α).HasBasis p s) {A B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) : ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
Full source 
theorem Disjoint.exists_uniform_thickening_of_basis {p : ι → Prop} {s : ι → Set (α × α)}
    (hU : (𝓤 α).HasBasis p s) {A B : Set α} (hA : IsCompact A) (hB : IsClosed B)
    (h : Disjoint A B) : ∃ i, p i ∧ Disjoint (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i)) := by
  rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩
  rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩
  exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a)
    (iUnion₂_mono fun b _ => ball_mono hiV b)⟩
Existence of Basis-Dependent Uniform Thickening for Disjoint Compact and Closed Sets
Informal description
Let $\alpha$ be a uniform space with a basis $\{s_i\}_{i \in \iota}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a predicate $p$. For any disjoint subsets $A$ and $B$ of $\alpha$ where $A$ is compact and $B$ is closed, there exists an index $i$ such that $p(i)$ holds and the uniform thickenings $\bigcup_{x \in A} \{y \in \alpha \mid (x, y) \in s_i\}$ and $\bigcup_{x \in B} \{y \in \alpha \mid (x, y) \in s_i\}$ are disjoint.
lebesgue_number_of_compact_open theorem
{K U : Set α} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ 𝓤 α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U
Full source 
/-- 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 lebesgue_number_of_compact_open {K U : Set α} (hK : IsCompact K)
    (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ 𝓤 α, IsOpen V ∧ ∀ x ∈ K, UniformSpace.ball x V ⊆ U :=
  let ⟨V, ⟨hV, hVo⟩, hVU⟩ :=
    (hK.nhdsSet_basis_uniformity uniformity_hasBasis_open).mem_iff.1 (hU.mem_nhdsSet.2 hKU)
  ⟨V, hV, hVo, iUnion₂_subset_iff.1 hVU⟩
Lebesgue Number Lemma for Compact Sets in Uniform Spaces
Informal description
Let $\alpha$ be a uniform space, $K \subseteq \alpha$ a compact subset, and $U \subseteq \alpha$ an open set containing $K$. Then there exists an open entourage $V$ in the uniformity $\mathfrak{U}(\alpha)$ such that for every $x \in K$, the uniform ball $\{y \in \alpha \mid (x, y) \in V\}$ is contained in $U$.
nhdsSet_diagonal_eq_uniformity theorem
[CompactSpace α] : 𝓝ˢ (diagonal α) = 𝓤 α
Full source 
/-- On a compact uniform space, the topology determines the uniform structure, entourages are
exactly the neighborhoods of the diagonal. -/
theorem nhdsSet_diagonal_eq_uniformity [CompactSpace α] : 𝓝ˢ (diagonal α) = 𝓤 α := by
  refine nhdsSet_diagonal_le_uniformity.antisymm ?_
  have :
    (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
      (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U := by
    rw [uniformity_prod_eq_comap_prod]
    exact (𝓤 α).basis_sets.prod_self.comap _
  refine (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => ?_
  exact mem_of_superset hU fun ⟨x, y⟩ hxy => mem_iUnion₂.2
    ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩
Neighborhood Filter of Diagonal Equals Uniformity in Compact Spaces
Informal description
For a compact uniform space $\alpha$, the neighborhood filter of the diagonal $\Delta_\alpha = \{(x,x) \mid x \in \alpha\}$ coincides with the uniformity filter $\mathfrak{U}(\alpha)$. In other words, the entourages of the uniformity are precisely the neighborhoods of the diagonal in the product space $\alpha \times \alpha$.
compactSpace_uniformity theorem
[CompactSpace α] : 𝓤 α = ⨆ x, 𝓝 (x, x)
Full source 
/-- On a compact uniform space, the topology determines the uniform structure, entourages are
exactly the neighborhoods of the diagonal. -/
theorem compactSpace_uniformity [CompactSpace α] : 𝓤 α = ⨆ x, 𝓝 (x, x) :=
  nhdsSet_diagonal_eq_uniformity.symm.trans (nhdsSet_diagonal _)
Uniformity Characterization in Compact Spaces: $\mathfrak{U}(\alpha) = \bigsqcup_{x} \mathcal{N}(x,x)$
Informal description
For a compact uniform space $\alpha$, the uniformity filter $\mathfrak{U}(\alpha)$ is equal to the supremum of the neighborhood filters at each point $(x,x)$ on the diagonal, i.e., \[ \mathfrak{U}(\alpha) = \bigsqcup_{x \in \alpha} \mathcal{N}(x,x). \]
unique_uniformity_of_compact theorem
[t : TopologicalSpace γ] [CompactSpace γ] {u u' : UniformSpace γ} (h : u.toTopologicalSpace = t) (h' : u'.toTopologicalSpace = t) : u = u'
Full source 
theorem unique_uniformity_of_compact [t : TopologicalSpace γ] [CompactSpace γ]
    {u u' : UniformSpace γ} (h : u.toTopologicalSpace = t) (h' : u'.toTopologicalSpace = t) :
    u = u' := by
  refine UniformSpace.ext ?_
  have : @CompactSpace γ u.toTopologicalSpace := by rwa [h]
  have : @CompactSpace γ u'.toTopologicalSpace := by rwa [h']
  rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']
Uniqueness of Uniformity on Compact Spaces
Informal description
Let $\gamma$ be a compact topological space with two uniform space structures $u$ and $u'$ such that both induce the same topology $t$ on $\gamma$. Then $u = u'$.