English
Expresses locally uniform convergence on a set in terms of punctured neighborhoods.
Русский
Выражение локально равномерной сходимости на множестве через зазубренные окрестности.
LaTeX
$$$\text{TendstoLocallyUniformlyOn}(F,f,p,s) \iff \forall \varepsilon>0, \forall x\in s, \exists t\in \mathcal{N}^{\neq}_x, \forall y\in t, edist(f y, F n y) < \varepsilon\, (предел по n).$$$
Lean4
/-- Expressing locally uniform convergence on a set using `edist`. -/
theorem tendstoLocallyUniformlyOn_iff {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι}
{s : Set β} :
TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε :=
by
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => ?_⟩
rcases mem_uniformity_edist.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)⟩
