Compact separated uniform spaces

Main statement

• uniformSpaceOfCompactR1: every compact R1 topological structure is induced by a uniform structure. This uniform structure is described by compactSpace_uniformity.

Implementation notes

The construction uniformSpaceOfCompactR1 is not declared as an instance, as it would badly loop.

Tags

uniform space, uniform continuity, compact space

Uniformity on compact spaces

def uniformSpaceOfCompactR1 {γ : Type u_1} [TopologicalSpace γ] [CompactSpace γ] [R1Space γ] : UniformSpace γ

The unique uniform structure inducing a given compact topological structure.

Equations

• uniformSpaceOfCompactR1 = { toTopologicalSpace := inst✝², uniformity := nhdsSet (Set.diagonal γ), symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }