gt_of_tendsto_zero_of_neg — Mathlib

English

If a sequence f(n) tends to 0, then for every positive real r, we have (r : ℝ*) < ofSeq f is impossible; rather, (-r) < ofSeq f holds.

Русский

Если 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 gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝 0)) : ∀ {r : ℝ}, r < 0 → (r : ℝ*) < ofSeq f :=
  fun {r} hr => by rw [← neg_neg r, coe_neg]; exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

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