Las sucesiones convergentes están acotadas
Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir,
\[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ} -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε -- (convergente u) expresa que u es convergente. def convergente (u : ℕ → ℝ) := ∃ a, limite u a example (h : convergente u) : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b := by sorry |