# mathlibdocumentation

topology.uniform_space.compact_separated

# 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 is compact_space.uniform_continuous_of_continuous.

## Implementation notes #

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

## tags #

uniform space, uniform continuity, compact space

### Uniformity on compact separated spaces #

theorem compact_space_uniformity {α : Type u_1}  :
= ⨆ (x : α), nhds (x, x)

On a separated compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.

theorem unique_uniformity_of_compact_t2 {γ : Type u_3} [t : topological_space γ] [t2_space γ] {u u' : uniform_space γ}  :
u = u'
def uniform_space_of_compact_t2 {γ : Type u_3} [t2_space γ] :

The unique uniform structure inducing a given compact Hausdorff topological structure.

Equations

### Heine-Cantor theorem #

theorem compact_space.uniform_continuous_of_continuous {α : Type u_1} {β : Type u_2} {f : α → β} (h : continuous f) :

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

theorem is_compact.uniform_continuous_on_of_continuous' {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} (hs : is_compact s) (hs' : is_separated s) (hf : s) :

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

theorem is_compact.uniform_continuous_on_of_continuous {α : Type u_1} {β : Type u_2} {s : set α} {f : α → β} (hs : is_compact s) (hf : s) :

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

theorem continuous_on.tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {x : α} {U : set α} (hxU : U nhds x) (hU : is_separated U) (h : (U ×ˢ set.univ)) :
(f x) (nhds x)

A family of functions α → β → γ tends uniformly to its value at x if α is locally compact, β is compact and separated and f is continuous on U × (univ : set β) for some separated neighborhood U of x.

theorem continuous.tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (h : continuous f) (x : α) :
(f x) (nhds x)

A continuous family of functions α → β → γ tends uniformly to its value at x if α is locally compact and β is compact and separated.