lt_of_tendsto_zero_of_pos — Mathlib

English

If a sequence f(n) tends to 0, then its hyperreal ofSeq is smaller than any positive real.

Русский

Если последовательность f(n) стремится к 0, то её гиперреальная запись ofSeq меньше любого положительного действительного числа.

LaTeX

$$$\\forall f:\\\\mathbb{N} \\\\to \\\\mathbb{R}, \\\\ Tendsto f \\\\atTop \\\\(\\\\mathcal{N} 0) \\\\Rightarrow \\\\forall {r:\\\\mathbb{R}}, 0 < r \\\\Rightarrow \\\\operatorname{ofSeq} f < (r : \\\\mathbb{R}^*)$$$

Lean4

theorem lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝 0)) : ∀ {r : ℝ}, 0 < r → ofSeq f < (r : ℝ*) :=
  fun hr ↦ ofSeq_lt_ofSeq.2 <| (hf.eventually <| gt_mem_nhds hr).filter_mono Nat.hyperfilter_le_atTop

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