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