Monotone_Convergence_Theorem_Real_Analysis
Provedlimits-of-sequencesmonotone-convergenceproofwiki
A monotone increasing sequence that is bounded above converges.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Order.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.Order.Basic theorem Monotone_Convergence_Theorem_Real_Analysis (x : ℕ → ℝ) (hm : Monotone x) (hb : BddAbove (Set.range x)) : ∃ l, Filter.Tendsto x Filter.atTop (nhds l) := by sorry
Source