En Lean, una sucesión \(a₀, a₁, a₂,...\) se puede representar mediante una función \(a : ℕ → ℝ\) de forma que \(a(n)\) es \(aₙ\).

Se define que \(L\) es el límite de la sucesión \(a\), por

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

Demostrar que si para todo \(n\), \(aₙ = 1/n\), entonces la sucesión \(a\) converge a 0.

Para ello, completar la siguiente teoría de Lean 4:

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

variable (a : ℕ → ℝ)

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

example
  (ha : ∀ n, a n = 1 / n)
  : SeqLim a 0 :=
by sorry

Leer más…