Compact separated uniform spaces

Main statement

• uniformSpace_of_compact_t2: every compact T2 topological structure is induced by a uniform structure. This uniform structure is described by compactSpace_uniformity.

Implementation notes

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

Tags

uniform space, uniform continuity, compact space

Uniformity on compact spaces

def uniformSpaceOfCompactT2 {γ : Type u_1} [TopologicalSpace γ] [CompactSpace γ] [T2Space γ] : UniformSpace γ

The unique uniform structure inducing a given compact topological structure.

Equations

• uniformSpaceOfCompactT2 = UniformSpace.mk (nhdsSet (Set.diagonal γ)) ⋯ ⋯ ⋯