tendsto_approx_atTop — Mathlib

English

The approximations converge to the limit uniformly along the natural filtration: c.approx n x tends to c.lim x as n → atTop.

Русский

Аппроксимации сходятся к предельному значению c.lim x при n → atTop.

LaTeX

$$$Tendsto(\\lambda n. c.approx n x)\\mathrm{atTop} (\\mathcal{N} (c.lim x))$$$

Lean4

theorem tendsto_approx_atTop (c : CU P) (x : X) : Tendsto (fun n => c.approx n x) atTop (𝓝 <| c.lim x) :=
  tendsto_atTop_ciSup (c.approx_mono x) ⟨1, fun _ ⟨_, hn⟩ => hn ▸ c.approx_le_one _ _⟩

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