19 febrero 2024 – Calculemus

Teorema del emparedado

PorJosé A. Alonso 19 febrero 202419 febrero 2024

Demostrar con Lean4 el teorema del emparedado.

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

import Mathlib.Data.Real.Basic

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

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

example
  (hu : limite u a)
  (hw : limite w a)
  (h1 : ∀ n, u n ≤ v n)
  (h2 : ∀ n, v n ≤ w n) :
  limite v a :=
by sorry

import Mathlib.Data.Real.Basic

variable (u v w : ℕ → ℝ)

variable (a : ℝ)

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

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

example

(hu : limite u a)

(hw : limite w a)

(h1 : ∀ n, u n ≤ v n)

(h2 : ∀ n, v n ≤ w n) :

limite v a :=

by sorry