tendsto_exp_atTop — Mathlib

English

exp tends to +∞ as x → +∞.

Русский

exp стремится к +∞ при x → +∞.

LaTeX

$$$$ \\lim_{x \\to +\\infty} \\exp x = +\\infty. $$$$

Lean4

/-- The real exponential function tends to `+∞` at `+∞`. -/
theorem tendsto_exp_atTop : Tendsto exp atTop atTop :=
  by
  have A : Tendsto (fun x : ℝ => x + 1) atTop atTop := tendsto_atTop_add_const_right atTop 1 tendsto_id
  have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩
  exact tendsto_atTop_mono' atTop B A

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