16 febrero 2024 – Calculemus

El límite de uₙ es a syss el de uₙ-a es 0

PorJosé A. Alonso 16 febrero 202419 febrero 2024

Demostrar con Lean4 que el límite de \(uₙ\) es \(a\) si, y sólo si, el de \(uₙ-a\) es \(0\).

Para ello, completar la siguiente teoría de Lean4:

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

variable  {u : ℕ → ℝ}
variable {a c x : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=
 fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  : limite u a ↔ limite (fun i ↦ u i - a) 0 :=
by sorry

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable {u : ℕ → ℝ}

variable {a c x : ℝ}

def limite : (ℕ → ℝ) → ℝ → Prop :=

fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example

: limite u a ↔ limite (fun i ↦ u i - a) 0 :=

by sorry