compactSpace_uniformity — Mathlib

English

If two uniform structures on a compact space induce the same topology, then they are equal.

Русский

Если две равномерные структуры на компактном пространстве порождают одну и ту же топологию, то они равны.

LaTeX

$$$$ \\text{If } [CompactSpace \\ γ] \\text{ and } u.toTopologicalSpace = u'.toTopologicalSpace,\\; u = u'. $$$$

Lean4

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

Похожие утверждения