15 febrero 2024 – Calculemus

Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca

PorJosé A. Alonso 15 febrero 202419 febrero 2024

Demostrar con Lean4 que si el límite de la sucesión \(uₙ\) es \(a\) y \(c ∈ ℝ\), entonces el límite de \(cuₙ\) es \(ca\).

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

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

variable (u v : ℕ → ℝ)
variable (a c : ℝ)

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

example
  (h : limite u a)
  : limite (fun n ↦ c * (u n)) (c * a) :=
by

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable (u v : ℕ → ℝ)

variable (a c : ℝ)

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

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

example

(h : limite u a)

: limite (fun n ↦ c * (u n)) (c * a) :=