Limit_of_Subsequence_of_Bounded_Sequence
Provedbounded-sequenceslimits-of-sequencesproofwiki
If a sequence is bounded by b, then any subsequential limit has absolute value at most b.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Subsequence_of_Bounded_Sequence (x : ℕ → ℝ) (b : ℝ) (hb : ∀ n, |x n| ≤ b) (phi : ℕ → ℕ) (hphi : StrictMono phi) (l : ℝ) (hl : Filter.Tendsto (x ∘ phi) Filter.atTop (nhds l)) : |l| ≤ b := by sorry
Source