Unicidad del límite de las sucesiones convergentes

En Lean, una sucesión $u₀, u₁, u₂, …$ se puede representar mediante una función $(u : ℕ → ℝ)$ de forma que $u(n)$ es $uₙ$ .

Se define que $a$ es el límite de la sucesión $u$ , por

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

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

Demostrar con Lean4 que cada sucesión tiene como máximo un límite.

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

import Mathlib.Data.Real.Basic
variable {u : ℕ → ℝ}
variable {a b : ℝ}

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

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
  by sorry

import Mathlib.Data.Real.Basic

variable {u : ℕ → ℝ}

variable {a b : ℝ}

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

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

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que si $u$ es una sucesión y $a$ y $b$ son límites de $u$ , entonces $a = b$ . Para ello, basta demostrar que $a ≤ b$ y $b ≤ a$ .

Demostraremos que $b ≤ a$ por reducción al absurdo. Supongamos que $b ≰ a$ . Sea $ε = b – a$ . Entonces, ε/2 > 0 y, puesto que $a$ es un límite de $u$ , existe un $A ∈ ℕ$ tal que
$(∀n ∈ ℕ)\left[n ≥ A → |u(n) – a| < \frac{ε}{2}\right] \tag{1}$
y, puesto que $b$ también es un límite de $u$ , existe un $B ∈ ℕ$ tal que
$(∀n ∈ ℕ)\left[n ≥ B → |u(n) – b| < \frac{ε}{2}\right] \tag{2}$
Sea $N = máx(A, B)$ . Entonces, $N ≥ A$ y $N ≥ B$ y, por (2) y (3), se tiene
$\begin{align} |u(N) – a| &< \frac{ε}{2} \tag{3} \\ |u(N) – b| &< \frac{ε}{2} \tag{4} \end{align}$
Para obtener una contradicción basta probar que $ε < ε$ . Su prueba es
$\begin{align} ε &= b – a \\ &= |b – a| \\ &= |(b – a) + (u(N) – u(N))| \\ &= |(u(N) – a) + (b – u(N))| \\ &≤ |u(N) – a| + |b – u(N)| \\ &= |u(N) – a| + |u(N) – b| \\ &< \frac{ε}{2} + \frac{ε}{2} && \text{[por (3) y (4)]} \\ &= ε \end{align}$

La demostración de $a ≤ b$ es análoga a la anterior.

2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable {u : ℕ → ℝ}
variable {a b : ℝ}

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

-- 1ª demostración del lema auxiliar
-- =================================

example
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
by
  by_contra h
  -- h : ¬b ≤ a
  -- ⊢ False
  let ε := b - a
  have hε : ε > 0 := sub_pos.mpr (not_le.mp h)
  have hε2 : ε / 2 > 0 := half_pos hε
  cases' ha (ε/2) hε2 with A hA
  -- A : ℕ
  -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2
  cases' hb (ε/2) hε2 with B hB
  -- B : ℕ
  -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2
  let N := max A B
  have hAN : A ≤ N := le_max_left A B
  have hBN : B ≤ N := le_max_right A B
  specialize hA N hAN
  -- hA : |u N - a| < ε / 2
  specialize hB N hBN
  -- hB : |u N - b| < ε / 2
  have h2 : ε < ε := by calc
    ε = b - a                   := rfl
    _ = |b - a|                 := (abs_of_pos hε).symm
    _ = |(b - a) + 0|           := by {congr ; exact (add_zero (b - a)).symm}
    _ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm}
    _ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring)
    _ ≤ |u N - a| + |b - u N|   := abs_add (u N - a) (b - u N)
    _ = |u N - a| + |u N - b|   := congrArg (|u N - a| + .) (abs_sub_comm b (u N))
    _ < ε / 2 + ε / 2           := add_lt_add hA hB
    _ = ε                       := add_halves ε
  have h3 : ¬(ε < ε) := lt_irrefl ε
  show False
  exact h3 h2

-- 2ª demostración del lema auxiliar
-- =================================

lemma aux
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
by
  by_contra h
  -- h : ¬b ≤ a
  -- ⊢ False
  let ε := b - a
  cases' ha (ε/2) (by linarith) with A hA
  -- A : ℕ
  -- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2
  cases' hb (ε/2) (by linarith) with B hB
  -- B : ℕ
  -- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2
  let N := max A B
  have hAN : A ≤ N := le_max_left A B
  have hBN : B ≤ N := le_max_right A B
  specialize hA N hAN
  -- hA : |u N - a| < ε / 2
  specialize hB N hBN
  -- hB : |u N - b| < ε / 2
  rw [abs_lt] at hA hB
  -- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2
  -- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2
  linarith

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

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (aux hb ha) (aux ha hb)

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

-- variable (c d : ℝ)
-- #check (not_le : ¬a ≤ b ↔ b < a)
-- #check (sub_pos : 0 < a - b ↔ b < a)
-- #check (half_pos : a > 0 → a / 2 > 0)
-- #check (le_max_left a b : a ≤ max a b)
-- #check (le_max_right a b : b ≤ max a b)
-- #check (abs_lt : |a| < b ↔ -b < a ∧ a < b)
-- #check (abs_of_pos : 0 < a → |a| = a)
-- #check (add_zero a : a + 0 = a)
-- #check (sub_self a : a - a = 0)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (abs_sub_comm a b : |a - b| = |b - a|)
-- #check (add_lt_add : a < b → c < d → a + c < b + d)
-- #check (add_halves a : a / 2 + a / 2 = a)
-- #check (lt_irrefl a : ¬a < a)
-- #check (le_antisymm : a ≤ b → b ≤ a → a = b)

100

101

102

103

104

105

106

import Mathlib.Data.Real.Basic

variable {u : ℕ → ℝ}

variable {a b : ℝ}

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

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

-- 1ª demostración del lema auxiliar

-- =================================

example

(ha : limite u a)

(hb : limite u b)

: b ≤ a :=

by_contra h

-- h : ¬b ≤ a

-- ⊢ False

let ε := b - a

have hε : ε > 0 := sub_pos.mpr (not_le.mp h)

have hε2 : ε / 2 > 0 := half_pos hε

cases' ha (ε/2) hε2 with A hA

-- A : ℕ

-- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2

cases' hb (ε/2) hε2 with B hB

-- B : ℕ

-- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2

let N := max A B

have hAN : A ≤ N := le_max_left A B

have hBN : B ≤ N := le_max_right A B

specialize hA N hAN

-- hA : |u N - a| < ε / 2

specialize hB N hBN

-- hB : |u N - b| < ε / 2

have h2 : ε < ε := by calc

ε = b - a := rfl

_ = |b - a| := (abs_of_pos hε).symm

_ = |(b - a) + 0| := by {congr ; exact (add_zero (b - a)).symm}

_ = |(b - a) + (u N - u N)| := by {congr ; exact (sub_self (u N)).symm}

_ = |(u N - a) + (b - u N)| := congrArg (fun x => |x|) (by ring)

_ ≤ |u N - a| + |b - u N| := abs_add (u N - a) (b - u N)

_ = |u N - a| + |u N - b| := congrArg (|u N - a| + .) (abs_sub_comm b (u N))

_ < ε / 2 + ε / 2 := add_lt_add hA hB

_ = ε := add_halves ε

have h3 : ¬(ε < ε) := lt_irrefl ε

show False

exact h3 h2

-- 2ª demostración del lema auxiliar

-- =================================

lemma aux

(ha : limite u a)

(hb : limite u b)

: b ≤ a :=

by_contra h

-- h : ¬b ≤ a

-- ⊢ False

let ε := b - a

cases' ha (ε/2) (by linarith) with A hA

-- A : ℕ

-- hA : ∀ (n : ℕ), n ≥ A → |u n - a| < ε / 2

cases' hb (ε/2) (by linarith) with B hB

-- B : ℕ

-- hB : ∀ (n : ℕ), n ≥ B → |u n - b| < ε / 2

let N := max A B

have hAN : A ≤ N := le_max_left A B

have hBN : B ≤ N := le_max_right A B

specialize hA N hAN

-- hA : |u N - a| < ε / 2

specialize hB N hBN

-- hB : |u N - b| < ε / 2

rw [abs_lt] at hA hB

-- hA : -(ε / 2) < u N - a ∧ u N - a < ε / 2

-- hB : -(ε / 2) < u N - b ∧ u N - b < ε / 2

linarith

-- 1ª demostración

-- ===============

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

le_antisymm (aux hb ha) (aux ha hb)

-- Lemas usados

-- ============

-- variable (c d : ℝ)

-- #check (not_le : ¬a ≤ b ↔ b < a)

-- #check (sub_pos : 0 < a - b ↔ b < a)

-- #check (half_pos : a > 0 → a / 2 > 0)

-- #check (le_max_left a b : a ≤ max a b)

-- #check (le_max_right a b : b ≤ max a b)

-- #check (abs_lt : |a| < b ↔ -b < a ∧ a < b)

-- #check (abs_of_pos : 0 < a → |a| = a)

-- #check (add_zero a : a + 0 = a)

-- #check (sub_self a : a - a = 0)

-- #check (abs_add a b : |a + b| ≤ |a| + |b|)

-- #check (abs_sub_comm a b : |a - b| = |b - a|)

-- #check (add_lt_add : a < b → c < d → a + c < b + d)

-- #check (add_halves a : a / 2 + a / 2 = a)

-- #check (lt_irrefl a : ¬a < a)

-- #check (le_antisymm : a ≤ b → b ≤ a → a = b)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory Unicidad_del_limite_de_las_sucesiones_convergentes
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

lemma aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed

theorem
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1) by (rule aux)
next
  show "b ≤ a" using assms(1) assms(2) by (rule aux)
qed

end

theory Unicidad_del_limite_de_las_sucesiones_convergentes

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

lemma aux :

assumes "limite u a"

"limite u b"

shows "b ≤ a"

proof (rule ccontr)

assume "¬ b ≤ a"

let ?ε = "b - a"

have "0 < ?ε/2"

using ‹¬ b ≤ a› by auto

obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"

using assms(1) limite_def ‹0 < ?ε/2› by blast

obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"

using assms(2) limite_def ‹0 < ?ε/2› by blast

let ?C = "max A B"

have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"

using hA by simp

have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"

using hB by simp

have "∀n≥?C. ¦a - b¦ < ?ε"

proof (intro allI impI)

fix n assume "n ≥ ?C"

have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp

also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp

finally show "¦a - b¦ < b - a"

using hCa hCb ‹n ≥ ?C› by fastforce

qed

then show False by fastforce

qed

theorem

assumes "limite u a"

"limite u b"

shows "a = b"

proof (rule antisym)

show "a ≤ b" using assms(2) assms(1) by (rule aux)

show "b ≤ a" using assms(1) assms(2) by (rule aux)

qed

end

1. Demostración en lenguaje natural

2. Demostraciones con Lean4

Demostraciones interactivas

3. Demostraciones con Isabelle/HOL

Share this:

Escribe un comentarioCancel reply