Theorems · Theorem · complex analysis
Real.tendsto_one_add_div_pow_exp
∀ (t : ℝ), Filter.Tendsto (fun n => (1 + t / ↑n) ^ n) Filter.atTop (nhds (Real.exp t))
The limit of (1 + t/n) ^ n as n → ∞ is exp t for t : ℝ.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 279 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- Real.expstatement · cited by 871
- Filter.Tendsto.compproof · cited by 560
- Real.rpow_natCastproof · cited by 93
- Filter.Tendsto.congrproof · cited by 70
- tendsto_natCast_atTop_atTopproof · cited by 51
- Real.tendsto_one_add_div_rpow_expproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- Complex.approx_Gamma_integral_tendsto_Gamma_integralproof · cited by 1
- tendsto_integral_mul_one_add_inv_smul_sq_powproof · cited by 1