Second_Subsequence_Rule
Provedmetric-spacesnamed-theoremsproofwiki
Let M be a metric space. Let (x_n) be a sequence with an unbounded subsequence. Then (x_n) does not converge.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Second_Subsequence_Rule {X : Type _} [MetricSpace X] {x : ℕ → X} (h : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ¬ Bornology.IsBounded (Set.range (x ∘ φ))) : ¬ ∃ L, Filter.Tendsto x Filter.atTop (nhds L) := by sorrySource