Theorems · Theorem · general topology

equicontinuous_iff_continuous

∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
  Equicontinuous F ↔ Continuous (⇑UniformFun.ofFun ∘ Function.swap F)

A family 𝓕 : ι → X → α is equicontinuous iff the function swap 𝓕 : X → ι → α is continuous when `ι → α` is equipped with the topology of uniform convergence. This is very useful for developing the equicontinuity API, but it should not be used directly for other purposes.

Defined in

Mathlib.Topology.UniformSpace.Equicontinuity

Cited by

4 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceUniformSpace