tendsto_one_add_div_pow_exp — Mathlib

English

For every real t, as n → ∞, (1 + t/n)^n → exp(t).

Русский

Пусть для каждого t ∈ ℝ, при n → ∞, выполняется (1 + t/n)^n → exp(t).

LaTeX

$$$$ \forall t \in \mathbb{R},\quad \lim_{n \to \infty} \left(1 + \frac{t}{n}\right)^n = \exp(t). $$$$

Lean4

/-- The limit of `(1 + t/n) ^ n` as `n → ∞` is `exp t` for `t : ℝ`. -/
theorem tendsto_one_add_div_pow_exp (t : ℝ) : Tendsto (fun n : ℕ ↦ (1 + t / n) ^ n) atTop (𝓝 (exp t)) :=
  tendsto_one_add_div_rpow_exp t |>.comp tendsto_natCast_atTop_atTop |>.congr (by simp)

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