tendstoLocallyUniformly_iff — Mathlib

English

Equivalent formulation of tendsto locally uniformly without sets via nhds.

Русский

Эквивалентная формулировка локальной равноупорядоченной сходимости без указания множеств через окрестности.

LaTeX

$$$\text{TendstoLocallyUniformly}(F,f,p) \iff \forall \varepsilon>0, \forall x, \exists t\in \mathcal{N}_x, \forall y\in t, edist(f y, F n y) < \varepsilon.$$

Lean4

/-- Expressing locally uniform convergence using `edist`. -/
theorem tendstoLocallyUniformly_iff {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} :
    TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε := by
  simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, mem_univ, forall_const, nhdsWithin_univ]

Похожие утверждения