English
Characterization of TendstoUniformlyOn/OnSet in terms of ε-criteria: TendstoUniformlyOn F f p s iff for all ε>0, ∀ x∈s, ∀ n∈p, dist(f x, F n x) < ε eventually.
Русский
Характеризация равномерного застывания на множестве в терминах ε: TendstoUniformlyOn F f p s эквивалентно тому, что для каждого ε>0 и каждого x∈s, dist(f x, F n x) < ε почти наверняка по n в p.
LaTeX
$$$\\text{TendstoUniformlyOn}(F,f,p,s) \\iff ∀ ε>0, ∀ x∈s, ∀^{\\infty}_{n∈p}, dist(f(x), F(n,x)) < ε$$$
Lean4
/-- Expressing uniform convergence on a set using `dist`. -/
theorem tendstoUniformlyOn_iff {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, dist (f x) (F n x) < ε :=
by
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)
