Theorems · Theorem · general topology

equicontinuousAt_iff_continuousAt

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

A family 𝓕 : ι → X → α is equicontinuous at x₀ iff the function swap 𝓕 : X → ι → α is continuous at x₀ 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

8 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpace