English
Expressing locally uniform convergence on a set: TendstoLocallyUniformlyOn F f p s iff for each ε>0 and x∈s there exists t ∈ 𝓝[s] x such that ∀ n in p, ∀ y ∈ t, dist(f y, F n y) < ε.
Русский
Локальная равномерная сходимость на множестве: для каждого ε>0 и каждого x∈s существует окрестность t внутри s такие, что для всех n в p, для всех y∈t выполняется dist(f y, F n y) < ε.
LaTeX
$$$\\text{TendstoLocallyUniformlyOn}(F,f,p,s) \\iff \\forall \\varepsilon>0, \\forall x\\in s, \\exists t ∈ \\mathcal{N}[s]x,\\; \\forall^{\\infty}_{n\\in p}, \\forall y∈t, dist(f(y), F(n,y)) < ε$$$
Lean4
/-- Expressing locally uniform convergence on a set using `dist`. -/
theorem tendstoLocallyUniformlyOn_iff [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} :
TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε :=
by
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
rcases H ε εpos x hx with ⟨t, ht, Ht⟩
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩
