Suppose that the sequence \(c_n\) is an interleaving of the sequences \(a_n\) and \(b_n\); that is, that \[ (c_0, c_1, c_2, \dots) = (a_0, b_0, a_1, b_1, a_2, b_2, \dots) \]

Prove that if \(c_n\) converges to \(L\), then \(a_n\) and \(b_n\) converge to \(L\).

To do so, complete the following theory

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. Collaborative solutions

How can you post your solution?

• Write your proof in live.lean-lang.org and check that it compiles without errors.
• Copy the code and post it in the comments of this entry, inside a Lean code block:

```lean
   -- your proof
```

• During the week you will be able to compare your approach with those of other participants. The official solution will be published on Monday 2 November 2026.