Demostrar que si la sucesión \(a_n\) converge a \(0\) y la sucesión \(b_n\) está acotada (no necesariamente es convergente), entonces la sucesión \(a_n·b_n\) converge a \(0\).

Para ello, completar la siguiente teoría

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

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 9 de noviembre de 2026.