La sucesión constante sₙ = c converge a c
En Lean, una sucesión \(s₀, s₁, s₂, …\) se puede representar mediante una función \(s : ℕ → ℝ\) de forma que \(s(n)\) es \(sₙ\).
Se define que a es el límite de la sucesión \(s\), por
|
1 2 |
def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε |
Demostrar que el límite de la sucesión constante \(sₙ = c\) es \(c\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic def limite (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε example : limite (fun _ : ℕ ↦ c) c := by sorry |