neg_lt_of_tendsto_zero_of_pos — Mathlib

English

If a sequence f(n) tends to 0, then for every positive real r, we have (-r) < ofSeq f.

Русский

Если f(n) стремится к 0, то для любого положительного числа r выполняется (-r) < ofSeq f.

LaTeX

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

Lean4

theorem neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝 0)) :
    ∀ {r : ℝ}, 0 < r → (-r : ℝ*) < ofSeq f := fun hr =>
  have hg := hf.neg
  neg_lt_of_neg_lt (by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr)

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