First_Subsequence_Rule
Provednamed-theoremsproofwikitopology
Let T be a Hausdorff space. Let (x_n) be a sequence in T with two convergent subsequences with different limits. Then (x_n) does not converge.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem First_Subsequence_Rule {X : Type _} [TopologicalSpace X] [T2Space X] {x : ℕ → X} {a b : X} (ha : ∃ φ : ℕ → ℕ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)) (hb : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ Filter.Tendsto (x ∘ ψ) Filter.atTop (nhds b)) (hab : a ≠ b) : ¬ Filter.Tendsto x Filter.atTop (nhds a) := by sorrySource