English
A family F is equicontinuous at x0 iff the swap F is continuous at x0 when indexed into the function space with the uniform convergence topology.
Русский
Семейство эконтинуировано в x0 тогда и тогда, когда его перестановка непрерывна в x0 в пространстве функций с топологией униформной сходимости.
LaTeX
$$$\\operatorname{EquicontinuousAt} F x_0 \\iff \\operatorname{ContinuousAt} (\\text{swap } F) x_0,$$$
Lean4
/-- 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. -/
theorem equicontinuousAt_iff_continuousAt {F : ι → X → α} {x₀ : X} :
EquicontinuousAt F x₀ ↔ ContinuousAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) x₀ :=
by
rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
rfl
