infinitesimal_of_tendsto_zero — Mathlib

English

If f: N → R tends to 0 along the natural numbers, then the hyperreal element ofSeq f is infinitesimal.

Русский

Пусть f: ℕ → ℝ удовлетворяет Tendsto f atTop (nhds 0); тогда гиперреальная величина ofSeq f∈Infinitesimal.

LaTeX

$$$ \operatorname{Tendsto}(f, \operatorname{atTop}, \mathcal{N}(0)) \Rightarrow \operatorname{Infinitesimal}(\operatorname{ofSeq}(f)) $$$

Lean4

theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} (h : Tendsto f atTop (𝓝 0)) : Infinitesimal (ofSeq f) :=
  isSt_of_tendsto h

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