isSt_of_tendsto — Mathlib

English

If a sequence f converges to r, then the hyperreal ofSeq f is infinitesimally close to r.

Русский

Если последовательность f сходится к r, то гиперреальная запись ofSeq f бесконечно близка к r.

LaTeX

$$Tendsto f atTop (nhds r) \\\\Rightarrow IsSt(ofSeq f) r$$

Lean4

theorem isSt_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : Tendsto f atTop (𝓝 r)) : IsSt (ofSeq f) r :=
  isSt_ofSeq_iff_tendsto.2 <| hf.mono_left Nat.hyperfilter_le_atTop

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