Convergence_of_Limsup_and_Liminf
Provedlimits-of-sequenceslimsup-liminfproofwiki
If limsup and liminf of a bounded sequence are equal, the sequence converges to that common value.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Order.LiminfLimsup
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Order.LiminfLimsup theorem Convergence_of_Limsup_and_Liminf (x : ℕ → ℝ) (l : ℝ) (hbdd : BddAbove (Set.range x) ∧ BddBelow (Set.range x)) (hsup : Filter.limsup x Filter.atTop = l) (hinf : Filter.liminf x Filter.atTop = l) : Filter.Tendsto x Filter.atTop (nhds l) := by sorry
Source