nat_tendsto_atTop — Mathlib

English

An injective sequence f: ℕ → ℕ tends to infinity, i.e., f(n) → atTop.

Русский

У инъективной последовательности f: ℕ → ℕ предел к бесконечности: f(n) растет к бесконечности.

LaTeX

$$$\\text{Injective}(f) \\Rightarrow \\operatorname{Tendsto} f \\operatorname{atTop} \\operatorname{atTop}$$$

Lean4

/-- An injective sequence `f : ℕ → ℕ` tends to infinity at infinity. -/
theorem nat_tendsto_atTop {f : ℕ → ℕ} (hf : Injective f) : Tendsto f atTop atTop :=
  Nat.cofinite_eq_atTop ▸ hf.tendsto_cofinite

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