tendsto_atTop — Mathlib

English

If φ is strictly increasing, then φ(n) tends to atTop as n→∞.

Русский

Если φ строго возрастает, то φ(n) стремится к верхней границе при n → ∞.

LaTeX

$$$$\forall φ: \mathbb{N} \to \mathbb{N}, \ \text{StrictMono } φ \Rightarrow \operatorname{Tendsto} φ\ \text{atTop}\ \text{atTop}. $$$$

Lean4

theorem _root_.StrictMono.tendsto_atTop {φ : ℕ → ℕ} (h : StrictMono φ) : Tendsto φ atTop atTop :=
  tendsto_atTop_mono h.id_le tendsto_id

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