English
For a compact space, the uniformity equals the supremum of the pointwise neighborhood filters along the diagonal: 𝓤 α = ⨆ x, 𝓝(x,x).
Русский
Для компактного пространства равномерности равны надмножеству диагонали: 𝓤 α = ⨆ x, 𝓝(x,x).
LaTeX
$$$$ 𝓤 \\alpha = \\bigsqcup_{x} 𝓝(x,x). $$$$
Lean4
/-- 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⟩
