English
Expressing uniform convergence on a filter: TendstoUniformlyOnFilter F f p p' iff for every ε>0, dist(f n.snd, F n.fst n.snd) < ε eventually in p×ˢ p'.
Русский
Выражение равномерного сходящегося по фильтру: TendstoUniformlyOnFilter F f p p' эквивалентно тому, что для каждого ε>0 расстояние между f и F меньше ε почти наверняка в произведении фильтров.
LaTeX
$$$\\text{TendstoUniformlyOnFilter}(F,f,p,p') \\iff \\forall \\varepsilon>0, \\forall^{\\infty} (n, x) \\in p \\times\\!\\! p',\, dist(f(x), F(n, x)) < \\varepsilon$$$
Lean4
/-- Expressing uniform convergence using `dist` -/
theorem tendstoUniformlyOnFilter_iff {F : ι → β → α} {f : β → α} {p : Filter ι} {p' : Filter β} :
TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ n : ι × β in p ×ˢ p', dist (f n.snd) (F n.fst n.snd) < ε :=
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 hn => hε hn
