Supongamos que la sucesión \(c_n\) es una mezcla de las sucesiones \(a_n\) y \(b_n\); es decir, que \[ (c_0, c_1, c_2, \dots) = (a_0, b_0, a_1, b_1, a_2, b_2, \dots) \]

Demostrar que si \(c_n\) converge a \(L\), entonces \(a_n\) y \(b_n\) convergen a \(L\).

Para ello, completar la siguiente teoría

import Mathlib.Tactic

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

example
  (hc : ∀ n, c n = if Even n
                   then a (n / 2)
                   else b ((n - 1) / 2))
  (hL : SeqLim c L)
  : SeqLim a L ∧ SeqLim b L :=
by sorry

3. Soluciones colaborativas

¿Cómo publicar tu solución?

• Escribe tu demostración en live.lean-lang.org y comprueba que se compila sin errores.
• Copia el código y publícalo en los comentarios de esta entrada, dentro de un bloque de código de Lean:

```lean
   -- tu demostración
```

• Durante la semana podrás comparar tu planteamiento con los de otros participantes. La solución oficial se publicará el lunes 2 de noviembre de 2026.