Limsup_Squeeze_Theorem
Provedanalysisdirect-proofsnamed-theoremsproofwiki
If |x_n| <= y_n for all n >= n_0 and limsup y_n = 0, then lim x_n = 0
Preamble
import Mathlib.Topology.Order.Basic import Mathlib.Topology.Algebra.Order.LiminfLimsup import Mathlib.Tactic
Formal statement
theorem Limsup_Squeeze_Theorem (x y : ℕ → ℝ) (n₀ : ℕ) (hxy : ∀ n, n₀ ≤ n → |x n| ≤ y n) (hy : Filter.Tendsto y Filter.atTop (nhds 0)) : Filter.Tendsto x Filter.atTop (nhds 0) := by sorry
Source