# Documentation

Mathlib.Topology.UniformSpace.Compact

# 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 #

theorem nhdsSet_diagonal_eq_uniformity {α : Type u_1} [] [] :

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

theorem compactSpace_uniformity {α : Type u_1} [] [] :
= ⨆ (x : α), nhds (x, x)

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

theorem unique_uniformity_of_compact {γ : Type u_3} [t : ] [] {u : } {u' : } (h : UniformSpace.toTopologicalSpace = t) (h' : UniformSpace.toTopologicalSpace = t) :
u = u'
def uniformSpaceOfCompactT2 {γ : Type u_3} [] [] [] :

The unique uniform structure inducing a given compact topological structure.

Instances For

### Heine-Cantor theorem

theorem CompactSpace.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (h : ) :

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

theorem IsCompact.uniformContinuousOn_of_continuous {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {f : αβ} (hs : ) (hf : ) :

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

theorem IsCompact.uniformContinuousAt_of_continuousAt {α : Type u_1} {β : Type u_2} [] [] {r : Set (β × β)} {s : Set α} (hs : ) (f : αβ) (hf : ∀ (a : α), a s) (hr : r ) :
{x | x.fst s(f x.fst, f x.snd) r}

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).

theorem Continuous.uniformContinuous_of_tendsto_cocompact {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : β} (h_cont : ) (hx : Filter.Tendsto f () (nhds x)) :
theorem HasCompactSupport.is_zero_at_infty {α : Type u_1} {γ : Type u_3} [] {f : αγ} [] [Zero γ] (h : ) :

If f has compact support, then f tends to zero at infinity.

theorem HasCompactMulSupport.is_one_at_infty {α : Type u_1} {γ : Type u_3} [] {f : αγ} [] [One γ] (h : ) :

If f has compact multiplicative support, then f tends to 1 at infinity.

theorem HasCompactSupport.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} [Zero β] (h1 : ) (h2 : ) :
theorem HasCompactMulSupport.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [] [] {f : αβ} [One β] (h1 : ) (h2 : ) :
theorem ContinuousOn.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : αβγ} {x : α} {U : Set α} (hxU : U nhds x) (h : ContinuousOn (f) (U ×ˢ Set.univ)) :

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.

theorem Continuous.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] (f : αβγ) (h : ) (x : α) :

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

theorem CompactSpace.uniformEquicontinuous_of_equicontinuous {α : Type u_1} {β : Type u_2} [] [] {ι : Type u_4} {F : ιβα} [] (h : ) :

An equicontinuous family of functions defined on a compact uniform space is automatically uniformly equicontinuous.