Compact separated uniform spaces #
Main statements #

compactSpace_uniformity
: On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal. 
uniformSpace_of_compact_t2
: every compact T2 topological structure is induced by a uniform structure. This uniform structure is described in the previous item. 
HeineCantor theorem: continuous functions on compact uniform spaces with values in uniform spaces are automatically uniformly continuous. There are several variations, the main one is
CompactSpace.uniformContinuous_of_continuous
.
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 #
On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.
On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.
The unique uniform structure inducing a given compact topological structure.
Equations
 uniformSpaceOfCompactT2 = UniformSpace.mk (nhdsSet (Set.diagonal γ)) ⋯ ⋯ ⋯
Instances For
### HeineCantor theorem
HeineCantor: a continuous function on a compact uniform space is uniformly continuous.
HeineCantor: a continuous function on a compact set of a uniform space is uniformly continuous.
If s
is compact and f
is continuous at all points of s
, then f
is
"uniformly continuous at the set s
", i.e. f x
is close to f y
whenever x ∈ s
and y
is
close to x
(even if y
is not itself in s
, so this is a stronger assertion than
UniformContinuousOn s
).
If f
has compact support, then f
tends to zero at infinity.
If f
has compact multiplicative support, then f
tends to 1 at infinity.
A family of functions α → β → γ
tends uniformly to its value at x
if α
is locally compact,
β
is compact and f
is continuous on U × (univ : Set β)
for some neighborhood U
of x
.
A continuous family of functions α → β → γ
tends uniformly to its value at x
if α
is weakly locally compact and β
is compact.
In a product space α × β
, assume that a function f
is continuous on s × k
where k
is
compact. Then, along the fiber above any q ∈ s
, f
is transversely uniformly continuous, i.e.,
if p ∈ s
is close enough to q
, then f p x
is uniformly close to f q x
for all x ∈ k
.
An equicontinuous family of functions defined on a compact uniform space is automatically uniformly equicontinuous.