Convergent_Subsequence_in_Closed_Interval
Provedcompactnesslimits-of-sequencesproofwiki
Every sequence in a closed interval [a,b] has a convergent subsequence whose limit is also in [a,b].
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Convergent_Subsequence_in_Closed_Interval (a b : ℝ) (x : ℕ → ℝ) (hx : ∀ n, a ≤ x n ∧ x n ≤ b) : ∃ (phi : ℕ → ℕ) (l : ℝ), StrictMono phi ∧ a ≤ l ∧ l ≤ b ∧ Filter.Tendsto (x ∘ phi) Filter.atTop (nhds l) := by sorry
Source