Compact separated uniform spaces #
Main statement #
uniformSpaceOfCompactR1: every compact R1 topological structure is induced by a uniform structure. This uniform structure is described bycompactSpace_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.