English
Uniform convergence on a set is characterized by uniform proximity of f(x) and F_n(x) for all x in that set.
Русский
Единообразная (uniform) сходимость на множестве охарактеризована близостью f(x) и F_n(x) на всем этом множестве.
LaTeX
$$$\text{TendstoUniformlyOn}(F,f,p,s) \iff \forall \varepsilon>0, \varepsilon\text{ положительно}, \forall x\in s, edist(f x, F_n x) < \varepsilon \text{ для больших n}.$$$
Lean4
/-- Expressing uniform convergence on a set using `edist`. -/
theorem tendstoUniformlyOn_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, edist (f x) (F n x) < ε :=
by
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)
