English
Equicontinuity at x0 is equivalent to the following: for every ε>0 there exists a neighborhood U of x0 such that for all x,x'∈U and all i, dist(F_i x, F_i x') < ε.
Русский
EquicontinuityAt F x0 эквивалентно существованию окрестности U x0, где для любых x,x'∈U и любого i выполняется dist(F_i x, F_i x') < ε для любого ε>0.
LaTeX
$$$ EquicontinuousAt F x_0 \iff \forall \varepsilon>0,\; \ exists U \in 𝓝(x_0),\; \forall x\in U, \forall x'\in U, \forall i,\; \mathrm{dist}(F_i x, F_i x') < \varepsilon. $$$
Lean4
/-- Characterization of equicontinuity for families of functions between (pseudo) metric spaces. -/
theorem equicontinuousAt_iff {ι : Type*} [PseudoMetricSpace β] {F : ι → β → α} {x₀ : β} :
EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x, dist x x₀ < δ → ∀ i, dist (F i x₀) (F i x) < ε :=
nhds_basis_ball.equicontinuousAt_iff uniformity_basis_dist
