Theorems · Theorem · general topology

equicontinuousWithinAt_iff_continuousWithinAt

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

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

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUniformSpace