English
If there exists a modulus function b with b → 0 at x0 and dist(F_i x0, F_i x) ≤ b(x) for x near x0 and all i, then F is equicontinuous at x0.
Русский
Если существует функция-модуль b, такая что b(x) → 0 при x → x0 и для близких x к x0 выполняется dist(F_i x0, F_i x) ≤ b(x) для всех i, то F равномерно непрерывно в x0.
LaTeX
$$$ \text{If } b:\beta\to\mathbb{R},\; \mathrm{Tendsto}(b,\mathcal{N}(x_0),\mathcal{N}(0))\text{ and } \forall x\to x_0,\; \forall i,\; \mathrm{dist}(F_i x_0, F_i x) \le b(x) \Rightarrow EquicontinuousAt F x_0. $$$
Lean4
/-- For a family of functions to a (pseudo) metric spaces, a convenient way to prove
equicontinuity at a point is to show that all of the functions share a common *local* continuity
modulus. -/
theorem equicontinuousAt_of_continuity_modulus {ι : Type*} [TopologicalSpace β] {x₀ : β} (b : β → ℝ)
(b_lim : Tendsto b (𝓝 x₀) (𝓝 0)) (F : ι → β → α) (H : ∀ᶠ x in 𝓝 x₀, ∀ i, dist (F i x₀) (F i x) ≤ b x) :
EquicontinuousAt F x₀ := by
rw [Metric.equicontinuousAt_iff_right]
intro ε ε0
filter_upwards [b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁
