tendstoUniformly_iff — Mathlib

English

Uniform convergence on the whole space is equivalent to pointwise convergence uniformly in the edist sense.

Русский

Равномерная сходимость на всей области эквивалентна униформной сходимости по edist.

LaTeX

$$$\text{TendstoUniformly}(F,f,p) \iff \forall \varepsilon>0, \forall x, edist(f x, F_n x) < \varepsilon \text{ eventually in } p$$$

Lean4

/-- Expressing uniform convergence using `edist`. -/
theorem tendstoUniformly_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : Filter ι} :
    TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, edist (f x) (F n x) < ε := by
  simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]

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