Compact separated uniform spaces #
Main statements #
compact_space_uniformity: On a separated compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.
uniform_space_of_compact_t2: every compact T2 topological structure is induced by a uniform structure. This uniform structure is described in the previous item.
- Heine-Cantor theorem: continuous functions on compact separated uniform spaces with values in
uniform spaces are automatically uniformly continuous. There are several variations, the main one
Implementation notes #
uniform_space_of_compact_t2 is not declared as an instance, as it would badly
uniform space, uniform continuity, compact space
Uniformity on compact separated spaces #
The unique uniform structure inducing a given compact Hausdorff topological structure.
Heine-Cantor theorem #
Heine-Cantor: a continuous function on a compact separated uniform space is uniformly continuous.
Heine-Cantor: a continuous function on a compact separated set of a uniform space is uniformly continuous.
Heine-Cantor: a continuous function on a compact set of a separated uniform space is uniformly continuous.