17 febrero 2024 – Calculemus

Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0

PorJosé A. Alonso 17 febrero 202419 febrero 2024

Demostrar con Lean4 que si \(uₙ\) y \(vₙ\) convergen a \(0\), entonces \(uₙvₙ\) converge a \(0\).

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

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

variable {u v : ℕ → ℝ}

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
by sorry

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable {u v : ℕ → ℝ}

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

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

by sorry