Reto 19: Las sucesiones convergentes son sucesiones de Cauchy

José A. Alonso

16-09-2026

El reto de esta semana consiste en demostrar en Lean 4 que las sucesiones convergentes son sucesiones de Cauchy

Para ello, completar la siguiente teoría de Lean 4:

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

variable {u : ℕ → ℝ}

def LimSuc (u : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def SucConvergente (u : ℕ → ℝ) :=
  ∃ a, LimSuc u a

def SucCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

example
  (h : SucConvergente u)
  : SucCauchy u :=
by sorry

1. Demostración en lenguaje natural

Sea \(\varepsilon \in \mathbb{R}\) tal que \(\varepsilon > 0\). Tenemos que demostrar que existe un \(k \in \mathbb{N}\) tal que \[ \forall p \geq k, \forall q \geq k, |u(p) - u(q)| < \varepsilon \tag{1} \]

Puesto que \(u\) es convergente, existe un \(a \in \mathbb{R}\) tal que el límite de \(u\) es \(a\). Por tanto, existe un \(k \in \mathbb{N}\) tal que \[ \forall n \geq k, |u(n) - a| < \dfrac{\varepsilon}{2} \tag{2} \]

Para demostrar que con dicho \(k\) se cumple (1), sean \(p, q \in \mathbb{N}\) tales que \(p \geq k\) y \(q \geq k\). Entonces, por (2), se tiene que \[ \begin{align} |u_p - a| &< \dfrac{\varepsilon}{2} \tag{3} \\ |u_q - a| &< \dfrac{\varepsilon}{2} \tag{4} \end{align} \] Por tanto, \[ \begin{array}{llll} |u_p - u_q| &= |(u_p - a) + (a - u_q)| \\ &≤ |u_p - a| + |a - u_q| \\ &= |u_p - a| + |u_q - a| \\ &< \dfrac{\varepsilon}{2} + \dfrac{\varepsilon}{2} &&\text{[por (3) y (4)]} \\ &= \varepsilon \end{array} \]

2. Demostraciones con Lean4

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

variable {u : ℕ → ℝ}

def LimSuc (u : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def SucConvergente (u : ℕ → ℝ) :=
  ∃ a, LimSuc u a

def SucCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

-- 1ª demostración
-- ===============

example
  (h : SucConvergente u)
  : SucCauchy u :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  obtain ⟨a, ha⟩ := h
  -- a : ℝ
  -- ha : LimSuc u a
  obtain ⟨k, hk⟩ := ha (ε/2) (by grind)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε / 2
  use k
  -- ⊢ ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  intros p hp q hq
  -- p : ℕ
  -- hp : p ≥ k
  -- q : ℕ
  -- hq : q ≥ k
  -- ⊢ |u p - u q| < ε
  grind

-- 2ª demostración
-- ===============

example
  (h : SucConvergente u)
  : SucCauchy u :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  obtain ⟨a, ha⟩ := h
  -- a : ℝ
  -- ha : LimSuc u a
  obtain ⟨k, hk⟩ := ha (ε/2) (by grind)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε / 2
  use k
  -- ⊢ ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  intros p hp q hq
  -- p : ℕ
  -- hp : p ≥ k
  -- q : ℕ
  -- hq : q ≥ k
  -- ⊢ |u p - u q| < ε
  calc |u p - u q|
       = |(u p - a) + (a - u q)| := by grind
     _ ≤ |u p - a|  + |a - u q|  := by grind
     _ = |u p - a|  + |u q - a|  := by grind
     _ < ε                       := by grind

-- 3ª demostración
-- ===============

example
  (h : SucConvergente u)
  : SucCauchy u :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  obtain ⟨a, ha⟩ := h
  -- a : ℝ
  -- ha : LimSuc u a
  obtain ⟨k, hk⟩ := ha (ε/2) (by positivity)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε / 2
  use k
  -- ⊢ ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  intros p hp q hq
  -- p : ℕ
  -- hp : p ≥ k
  -- q : ℕ
  -- hq : q ≥ k
  -- ⊢ |u p - u q| < ε
  have h1 : |u p - a| < ε / 2 := hk p hp
  have h2 : |u q - a| < ε / 2 := hk q hq
  calc |u p - u q|
       = |(u p - a) + (a - u q)| := by ring_nf
     _ ≤ |u p - a| + |a - u q|   := abs_add_le _ _
     _ = |u p - a| + |u q - a|   := by simp [abs_sub_comm]
     _ < ε / 2 + ε / 2           := by gcongr
     _ = ε                       := by ring

-- 4ª demostración
-- ===============

example
  (h : SucConvergente u)
  : SucCauchy u :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  obtain ⟨a, ha⟩ := h
  -- a : ℝ
  -- ha : LimSuc u a
  obtain ⟨k, hk⟩ := ha (ε/2) (half_pos hε)
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε / 2
  use k
  -- ⊢ ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε
  intros p hp q hq
  -- p : ℕ
  -- hp : p ≥ k
  -- q : ℕ
  -- hq : q ≥ k
  -- ⊢ |u p - u q| < ε
  calc |u p - u q|
       = |(u p - a) + (a - u q)| :=
           congrArg abs (sub_add_sub_cancel (u p) a (u q)).symm
     _ ≤ |u p - a|  + |a - u q| :=
           abs_add_le (u p - a) (a - u q)
     _ = |u p - a|  + |u q - a| :=
           congrArg (|u p - a| + ·) (abs_sub_comm a (u q))
     _ < ε / 2 + ε / 2 :=
           add_lt_add (hk p hp) (hk q hq)
     _ = ε :=
           add_halves ε

-- Lemas usados
-- ============

variable (a b c d : ℝ)
variable (f : ℝ → ℝ)
#check (abs_add_le a b : |a + b| ≤ |a| + |b|)
#check (abs_sub_comm a b : |a - b| = |b - a|)
#check (add_halves a : a / 2 + a / 2 = a)
#check (add_left_cancel_iff : a + b = a + c ↔ b = c)
#check (add_lt_add : a < b → c < d → a + c < b + d)
#check (congrArg f : a = b → f a = f b)
#check (half_pos : 0 < a → 0 < a / 2)
#check (sub_add_sub_cancel a b c : (a - b) + (b - c) = a - c)

En el siguiente vídeo se explica paso a paso la construcción de las soluciones:

Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.