# 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.**Heine-Cantor**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

### Heine-Cantor theorem #

Heine-Cantor: a continuous function on a compact uniform space is uniformly continuous.

Heine-Cantor: 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`

).

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.