English
Uniform equicontinuity of F is equivalent to: for every ε>0, the set of pairs (x,y) close in the uniformity implies dist(F_i x, F_i y) < ε for all i.
Русский
Единое равномерное экв-cont семейства F эквивалентно тому, что для каждого ε>0 множество пар (x,y), близких по униформности, удовлетворяет dist(F_i x, F_i y) < ε для всех i.
LaTeX
$$$ UniformEquicontinuous F \iff \forall \varepsilon>0,\; \forall (x,y)\text{ with } (x,y)\to\text{close},\; \forall i,\; \mathrm{dist}(F_i x, F_i y) < \varepsilon. $$$
Lean4
/-- Characterization of uniform equicontinuity for families of functions between
(pseudo) metric spaces. -/
theorem uniformEquicontinuous_iff {ι : Type*} [PseudoMetricSpace β] {F : ι → β → α} :
UniformEquicontinuous F ↔ ∀ ε > 0, ∃ δ > 0, ∀ x y, dist x y < δ → ∀ i, dist (F i x) (F i y) < ε :=
uniformity_basis_dist.uniformEquicontinuous_iff uniformity_basis_dist
