One_Plus_Reciprocal_to_the_Nth
Provedlimits-of-sequencesproofwiki
The sequence (1 + 1/n)^n converges to a limit (Euler's number e).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem One_Plus_Reciprocal_to_the_Nth : ∃ l : ℝ, Filter.Tendsto (fun n : ℕ => (1 + 1 / ((n : ℝ) + 1)) ^ (n + 1)) Filter.atTop (nhds l) := by sorry
Source