Using Challenge 22 (which states that if a sequence has two subsequences converging to different limits, then the sequence is not convergent), prove that the sequence defined by 1, -1, 1, -1, ... is not convergent.

To do so, complete the following theory:

import Mathlib.Tactic

-- a converges to L
def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

-- The sequence a is convergent
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b is a subsequence of a.
def Subseq (b a : ℕ → ℝ) : Prop :=
  ∃ φ, IsExtraction φ ∧ b = a ∘ φ

variable {a : ℕ → ℝ}

example
  (ha : ∀ n, a n = (-1)^n)
  : ¬SeqConv a :=
by sorry

How to publish your solution?

1. Write your proof at live.lean-lang.org and copy the link it generates.
2. Post it in the Mastodon thread for this problem, with a message like:
   “My solution is at [link].”
3. You will be able to compare your approach with those of other participants during the week. The official solution will be published next Monday.