English
On a compact space, the neighborhoods of the diagonal equal the uniformity; the topology determines the uniform structure.
Русский
На компактном пространстве окрестности диагонали равны равномерности; топология определяет равномерную структуру.
LaTeX
$$$$ 𝓝ˢ(\\Delta α) = 𝓤 α \\quad\\text{ for compact } α.$$$$
Lean4
/-- 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⟩
