Usando el Reto 22 (que afirma que si una sucesión tiene dos subsucesiones que convergen a límites distintos, entonces la sucesión no es convergente) demostrar que la sucesión definida por 1, -1, 1, -1, ... no es convergente.

Para ello, completar la siguiente teoría:

import Mathlib.Tactic

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

-- La sucesión a es convergente
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

-- φ es una función de extracción.
def IsExtraction (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b es una subsucesión de a.
def Subseq (b a : ℕ → ℝ) : Prop :=
  ∃ φ, IsExtraction φ ∧ b = a ∘ φ

variable {a : ℕ → ℝ}

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

¿Cómo publicar tu solución?

1. Escribe tu demostración en live.lean-lang.org y copia el enlace que genera.
2. Publícalo en el hilo de Mastodon de este problema, con un mensaje del tipo:
   «Mi solución está en [enlace].»
3. Podrás comparar tu planteamiento con el de otros participantes durante la semana. La solución oficial se publicará el próximo lunes.