English
If a family F satisfies a global modulus bound dist(F_i x, F_i y) ≤ b(dist x y) for all x,y and i, with b → 0 as dist x y → 0, then F is equicontinuous.
Русский
Если для всех x,y и i выполняется неравенство dist(F_i x, F_i y) ≤ b(dist x y) при некотором глобальном модуле b, и b → 0 при dist x y → 0, то F равномерно эквивалентно.
LaTeX
$$$ \text{If } \forall x,y,i,\; \mathrm{dist}(F_i x, F_i y) \le b(\mathrm{dist}(x,y))\text{ with } \lim_{t\to 0} b(t)=0, \text{ then } UniformEquicontinuous F. $$$
Lean4
/-- For a family of functions between (pseudo) metric spaces, a convenient way to prove
equicontinuity is to show that all of the functions share a common *global* continuity modulus. -/
theorem equicontinuous_of_continuity_modulus {ι : Type*} [PseudoMetricSpace β] (b : ℝ → ℝ)
(b_lim : Tendsto b (𝓝 0) (𝓝 0)) (F : ι → β → α) (H : ∀ (x y : β) (i), dist (F i x) (F i y) ≤ b (dist x y)) :
Equicontinuous F :=
(uniformEquicontinuous_of_continuity_modulus b b_lim F H).equicontinuous
