Documentation

Mathlib.Topology.UniformSpace.Compact

Compact separated uniform spaces #

Main statements #

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.

theorem compactSpace_uniformity {α : Type u_1} [UniformSpace α] [CompactSpace α] :
uniformity α = ⨆ (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 : TopologicalSpace γ] [CompactSpace γ] {u : UniformSpace γ} {u' : UniformSpace γ} (h : UniformSpace.toTopologicalSpace = t) (h' : UniformSpace.toTopologicalSpace = t) :
u = u'

The unique uniform structure inducing a given compact topological structure.

Equations
Instances For

    ### Heine-Cantor theorem

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

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

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

    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} [UniformSpace α] [UniformSpace β] {r : Set (β × β)} {s : Set α} (hs : IsCompact s) (f : αβ) (hf : as, ContinuousAt f a) (hr : r uniformity β) :
    {x : α × α | x.1 s(f x.1, f x.2) r} uniformity α

    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} [UniformSpace α] [UniformSpace β] {f : αβ} {x : β} (h_cont : Continuous f) (hx : Filter.Tendsto f (Filter.cocompact α) (nhds x)) :
    theorem HasCompactSupport.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : αβ} [Zero β] (h1 : HasCompactSupport f) (h2 : Continuous f) :
    theorem ContinuousOn.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace α] [UniformSpace β] [LocallyCompactSpace α] [CompactSpace β] [UniformSpace γ] {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} [UniformSpace α] [UniformSpace β] [WeaklyLocallyCompactSpace α] [CompactSpace β] [UniformSpace γ] (f : αβγ) (h : Continuous f) (x : α) :

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

    theorem IsCompact.mem_uniformity_of_prod {α : Type u_4} {β : Type u_5} {E : Type u_6} [TopologicalSpace α] [TopologicalSpace β] [UniformSpace E] {f : αβE} {s : Set α} {k : Set β} {q : α} {u : Set (E × E)} (hk : IsCompact k) (hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)) (hq : q s) (hu : u uniformity E) :
    vnhdsWithin q s, pv, xk, (f p x, f q x) u

    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.

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

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