English
Characterize equicontinuity of a family of functions F: ι → β → α from β to a metric space α: EquicontinuousAt F at x0 holds exactly when, for every ε>0, there is a neighborhood basis element around x0 such that for all x in that neighborhood and all i, dist(F_i x0, F_i x) < ε.
Русский
Характеризовать равномерную непрерывность семейства функций F: ι → β → α через окрестности точки x0: EquicontinuousAt F x0 эквивалентно тому, что для любого ε>0 существует окрестность U вокруг x0, такая что для всех x∈U и всех i dist(F_i x0, F_i x) < ε.
LaTeX
$$$ EquicontinuousAt F x_0 \quad\Leftrightarrow\quad \forall \varepsilon>0,\; \forall x \text{ near } x_0,\; \forall i,\; \mathrm{dist}(F_i x_0, F_i x) < \varepsilon, $$$
Lean4
/-- Characterization of equicontinuity for families of functions taking values in a (pseudo) metric
space. -/
theorem equicontinuousAt_iff_right {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {x₀ : β} :
EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∀ᶠ x in 𝓝 x₀, ∀ i, dist (F i x₀) (F i x) < ε :=
uniformity_basis_dist.equicontinuousAt_iff_right
