24 mayo 2024 – Calculemus

Los supremos de las sucesiones crecientes son sus límites

PorJosé A. Alonso 24 mayo 202422 mayo 2024

Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).

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

import Mathlib.Data.Real.Basic

variable (u : ℕ → ℝ)
variable (S : ℝ)

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε

-- (supremo u S) expresa que el supremo de u es S.
def supremo (u : ℕ → ℝ) (S : ℝ) :=
  (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by sorry

import Mathlib.Data.Real.Basic

variable (u : ℕ → ℝ)

variable (S : ℝ)

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε

-- (supremo u S) expresa que el supremo de u es S.

def supremo (u : ℕ → ℝ) (S : ℝ) :=

(∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε

example

(hu : Monotone u)

(hS : supremo u S)

: limite u S :=

by sorry