Lower_and_Upper_Bounds_for_Sequences
Provedlimits-of-sequencesproofwiki
If a sequence x_n converges to l and a <= x_n for all n, then a <= l.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Lower_and_Upper_Bounds_for_Sequences (x : ℕ → ℝ) (l : ℝ) (h : Filter.Tendsto x Filter.atTop (nhds l)) (a : ℝ) (ha : ∀ n, a ≤ x n) : a ≤ l := by sorry
Source