English
A family F: ι → β → α is uniformly equicontinuous if and only if for every ε>0, there exists a neighborhood around every pair in the product basis such that the images under all F_i are within ε.
Русский
Семейство F: ι → β → α удовлетворяет условию равномерной экв-cont iff для каждого ε>0 существует общая окрестность, в которой расстояния между образами F_i лежат в пределах ε.
LaTeX
$$$ UniformEquicontinuous F \iff \forall \varepsilon>0,\; \forall \text{basis neighborhoods } U \text{ of } β\timesβ,\; \forall i,\; \mathrm{dist}(F_i x, F_i y) < \varepsilon \text{ for all } (x,y)\in U. $$$
Lean4
/-- Characterization of uniform equicontinuity for families of functions taking values in a
(pseudo) metric space. -/
theorem uniformEquicontinuous_iff_right {ι : Type*} [UniformSpace β] {F : ι → β → α} :
UniformEquicontinuous F ↔ ∀ ε > 0, ∀ᶠ xy : β × β in 𝓤 β, ∀ i, dist (F i xy.1) (F i xy.2) < ε :=
uniformity_basis_dist.uniformEquicontinuous_iff_right
