tendstoUniformly_iff_tendsto — Mathlib

English

TendstoUniformly F f p is equivalent to Tendsto (f, F) along p ×⊤ to 𝓤(β).

Русский

Сходимость F к f по p равносильна стремлению пары (f, F) вдоль p ×⊤ к 𝓤(β).

LaTeX

$$$$TendstoUniformly(F,f,p)\\iff Tendsto(\\lambda q:(ι\\times α). (f(q.2), F q.1 q.2)) (p \\timesˢ ⊤) (𝓤(β)).$$$$

Lean4

/-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` w.r.t.
filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ ⊤` to the uniformity.
In other words: one knows nothing about the behavior of `x` in this limit.
-/
theorem tendstoUniformly_iff_tendsto :
    TendstoUniformly F f p ↔ Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β) := by
  simp [tendstoUniformly_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

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