English
UniformEquicontinuous F is equivalent to the equality with a Continuous mapping after swap.
Русский
Равномерно эконтинуированное семейство эквивалентно непрерывности после перестановки.
LaTeX
$$$\\operatorname{UniformEquicontinuous} F \\iff \\operatorname{Continuous} (\\text{ofFun} \\circ \\text{Function.swap } F).$$$
Lean4
/-- 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. -/
theorem equicontinuous_iff_continuous {F : ι → X → α} :
Equicontinuous F ↔ Continuous (ofFun ∘ Function.swap F : X → ι →ᵤ α) := by
simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]
