English
If there is a real-valued modulus b with b → 0 and a family F with dist(F_i x, F_i y) ≤ b(dist x y) for all i, then F is uniformly equicontinuous.
Русский
Если существует модуль b и семейство F такое, что dist(F_i x, F_i y) ≤ b(dist(x,y)) для всех i, то F является uniformly equicontinuous.
LaTeX
$$$ UniformEquicontinuous F \iff \forall \varepsilon>0,\; \forall δ>0,\; \forall x,y,\; d(x,y)<δ \Rightarrow d(F_i x, F_i y)<ε. $$$
Lean4
/-- For a family of functions between (pseudo) metric spaces, a convenient way to prove
uniform equicontinuity is to show that all of the functions share a common *global* continuity
modulus. -/
theorem uniformEquicontinuous_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)) :
UniformEquicontinuous F := by
rw [Metric.uniformEquicontinuous_iff]
intro ε ε0
rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩
refine ⟨δ, δ0, fun x y hxy i => ?_⟩
calc
dist (F i x) (F i y) ≤ b (dist x y) := H x y i
_ ≤ |b (dist x y)| := (le_abs_self _)
_ = dist (b (dist x y)) 0 := by simp [Real.dist_eq]
_ < ε := hδ (by simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy)
