Prove that if the sequence \(a_n\) converges to \(0\) and the sequence \(b_n\) is bounded (not necessarily convergent), then the sequence \(a_n·b_n\) converges to \(0\).

To do so, complete the following theory

import Mathlib.Basic.Real.Basic
import Mathlib.Tactic

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

def SeqBdd (a : ℕ → ℝ) : Prop :=
  ∃ M > 0, ∀ n, |a n| ≤ M

variable (a b : ℕ → ℝ)

example
  (ha : SeqLim a 0)
  (hb : SeqBdd b)
  : SeqLim (a * b) 0 :=
by sorry

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 Monday 9 November 2026.