English
Locally uniform convergence on the whole space: TendstoLocallyUniformly F f p iff ∀ ε>0, ∀ x, ∃ t ∈ 𝓝 x, ∀ y∈t, dist(f y, F n y) < ε eventually in p.
Русский
Локальная равномерная сходимость на всём пространстве: эквивалентно существованию окрестности вокруг каждого x, где сближение происходит равномерно.
LaTeX
$$$\\text{TendstoLocallyUniformly}(F,f,p) \\iff ∀ ε>0, ∀ x, ∃ t ∈ \\mathcal{N}x, \\; \\forall^{\\infty}_{n∈p}, \\forall y∈t, dist(f y, F(n,y)) < ε$$$
Lean4
/-- Expressing locally uniform convergence using `dist`. -/
theorem tendstoLocallyUniformly_iff [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} :
TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε := by
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, nhdsWithin_univ, mem_univ, forall_const]
