English
A reformulation of equicontinuity at x0 for a family of functions into a metric space asserts that F is equicontinuous at x0 iff, for every ε>0, there exists a neighborhood U of x0 such that for all x,x'∈U and i, dist(F_i x, F_i x') < ε.
Русский
Переформулируя равномерную непрерывность через пары точек: F равномерно непрерывна в x0 тогда и только тогда, для каждого ε>0 существует окрестность U x0, такая что для всех x,x'∈U и для всех i выполняется dist(F_i x, F_i x') < ε.
LaTeX
$$$ EquicontinuousAt F x_0 \iff \forall \varepsilon>0, \; \exists U \in 𝓝(x_0),\; \forall x\in U, \forall x'\in U, \forall i,\; \mathrm{dist}(F_i x, F_i x') < \varepsilon. $$$
Lean4
/-- Reformulation of `equicontinuousAt_iff_pair` for families of functions taking values in a
(pseudo) metric space. -/
protected theorem equicontinuousAt_iff_pair {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {x₀ : β} :
EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ i, dist (F i x) (F i x') < ε :=
by
rw [equicontinuousAt_iff_pair]
constructor <;> intro H
· intro ε hε
exact H _ (dist_mem_uniformity hε)
· intro U hU
rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
refine Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)
exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)
