tendsto_of_eventually_tendsto — Mathlib

English

If TendstoUniformlyOnFilter F f p p' and ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i)) and Tendsto L p (𝓝 ℓ), then Tendsto f p' (𝓝 ℓ).

Русский

Если есть равномерное сходящееся по фильтру на предикаторе F и f, причём для большинства i в p выполняется предел F i, и L стремится к ℓ, тогда f стремится к ℓ.

LaTeX

$$$\\text{TendstoUniformlyOnFilter } F f p p' \\to \\big(\\forallᶠ i \\text{ in } p, \\ Tendsto (F i) p' (\\mathcal{nhds} (L i))\\big) \\to \\ big(\\text{Tendsto } L p (\\mathcal{nhds} \\ell) \\to \\text{Tendsto } f p' (\\mathcal{nhds} \\ell)\\big)$$$

Lean4

theorem tendsto_of_eventually_tendsto (h1 : TendstoUniformly F f p) (h2 : ∀ᶠ i in p, Tendsto (F i) p' (𝓝 (L i)))
    (h3 : Tendsto L p (𝓝 ℓ)) : Tendsto f p' (𝓝 ℓ) :=
  (h1.tendstoUniformlyOnFilter.mono_right le_top).tendsto_of_eventually_tendsto h2 h3

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