Ir al contenido principal

La semana en Calculemus (2 de junio de 2024)

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

A continuación se muestran las soluciones.

1. Un número es par si y solo si lo es su cuadrado

Demostrar con Lean4 que un número es par si y solo si lo es su cuadrado.

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

import Mathlib.Data.Int.Parity
import Mathlib.Tactic
open Int

variable (n : ℤ)

example :
  Even (n^2) ↔ Even n :=
by sorry

1.1. Demostración en lenguaje natural

Sea \(n ∈ ℤ\). Tenemos que demostrar que \(n^2\) es par si y solo si n es par. Lo haremos probando las dos implicaciones.

(⟹) Lo demostraremos por contraposición. Para ello, supongamos que \(n\) no es par. Entonces, existe un \(k ∈ Z\) tal que \[ n = 2k+1 \tag{1} \] Luego, \begin{align} n^2 &= (2k+1)^2 &&\text{[por (1)]} \newline &= 4k^2+4k+1 \newline &= 2(2k(k+1))+1 \end{align} Por tanto, \(n^2\) es impar.

(⟸) Supongamos que \(n\) es par. Entonces, existe un \(k ∈ ℤ\) tal que \[ n = 2k \tag{2} \] Luego, \begin{align} n^2 &= (2k)^2 &&\text{[por (2)]} \newline &= 2(2k^2) \end{align} Por tanto, \(n^2\) es par.

1.2. Demostraciones con Lean4

import Mathlib.Data.Int.Parity
import Mathlib.Tactic
open Int

variable (n : ℤ)

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

example :
  Even (n^2) ↔ Even n :=
by
  constructor
  . -- ⊢ Even (n ^ 2) → Even n
    contrapose
    -- ⊢ ¬Even n → ¬Even (n ^ 2)
    intro h
    -- h : ¬Even n
    -- ⊢ ¬Even (n ^ 2)
    rw [←odd_iff_not_even] at *
    -- h : Odd n
    -- ⊢ Odd (n ^ 2)
    cases' h with k hk
    -- k : ℤ
    -- hk : n = 2 * k + 1
    use 2*k*(k+1)
    -- ⊢ n ^ 2 = 2 * (2 * k * (k + 1)) + 1
    calc n^2
         = (2*k+1)^2       := by rw [hk]
       _ = 4*k^2+4*k+1     := by ring
       _ = 2*(2*k*(k+1))+1 := by ring
  . -- ⊢ Even n → Even (n ^ 2)
    intro h
    -- h : Even n
    -- ⊢ Even (n ^ 2)
    cases' h with k hk
    -- k : ℤ
    -- hk : n = k + k
    use 2*k^2
    -- ⊢ n ^ 2 = 2 * k ^ 2 + 2 * k ^ 2
    calc n^2
         = (k + k)^2     := by rw [hk]
       _ = 2*k^2 + 2*k^2 := by ring

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

example :
  Even (n^2) ↔ Even n :=
by
  constructor
  . -- ⊢ Even (n ^ 2) → Even n
    contrapose
    -- ⊢ ¬Even n → ¬Even (n ^ 2)
    rw [←odd_iff_not_even]
    -- ⊢ Odd n → ¬Even (n ^ 2)
    rw [←odd_iff_not_even]
    -- ⊢ Odd n → Odd (n ^ 2)
    unfold Odd
    -- ⊢ (∃ k, n = 2 * k + 1) → ∃ k, n ^ 2 = 2 * k + 1
    intro h
    -- h : ∃ k, n = 2 * k + 1
    -- ⊢ ∃ k, n ^ 2 = 2 * k + 1
    cases' h with k hk
    -- k : ℤ
    -- hk : n = 2 * k + 1
    use 2*k*(k+1)
    -- ⊢ n ^ 2 = 2 * (2 * k * (k + 1)) + 1
    rw [hk]
    -- ⊢ (2 * k + 1) ^ 2 = 2 * (2 * k * (k + 1)) + 1
    ring
  . -- ⊢ Even n → Even (n ^ 2)
    unfold Even
    -- ⊢ (∃ r, n = r + r) → ∃ r, n ^ 2 = r + r
    intro h
    -- h : ∃ r, n = r + r
    -- ⊢ ∃ r, n ^ 2 = r + r
    cases' h with k hk
    -- k : ℤ
    -- hk : n = k + k
    use 2*k^2
    -- ⊢ n ^ 2 = 2 * k ^ 2 + 2 * k ^ 2
    rw [hk]
    -- ⊢ (k + k) ^ 2 = 2 * k ^ 2 + 2 * k ^ 2
    ring

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

example :
  Even (n^2) ↔ Even n :=
by
  constructor
  . -- ⊢ Even (n ^ 2) → Even n
    contrapose
    -- ⊢ ¬Even n → ¬Even (n ^ 2)
    rw [←odd_iff_not_even]
    -- ⊢ Odd n → ¬Even (n ^ 2)
    rw [←odd_iff_not_even]
    -- ⊢ Odd n → Odd (n ^ 2)
    rintro ⟨k, rfl⟩
    -- k : ℤ
    -- ⊢ Odd ((2 * k + 1) ^ 2)
    use 2*k*(k+1)
    -- ⊢ (2 * k + 1) ^ 2 = 2 * (2 * k * (k + 1)) + 1
    ring
  . -- ⊢ Even n → Even (n ^ 2)
    rintro ⟨k, rfl⟩
    -- k : ℤ
    -- ⊢ Even ((k + k) ^ 2)
    use 2*k^2
    -- ⊢ (k + k) ^ 2 = 2 * k ^ 2 + 2 * k ^ 2
    ring

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

example :
  Even (n^2) ↔ Even n :=
calc Even (n^2)
     ↔ Even (n * n)      := iff_of_eq (congrArg Even (sq n))
   _ ↔ (Even n ∨ Even n) := even_mul
   _ ↔ Even n            := or_self_iff (Even n)

-- 5ª demostración
-- ===============

example :
  Even (n^2) ↔ Even n :=
calc Even (n^2)
     ↔ Even (n * n)      := by ring_nf
   _ ↔ (Even n ∨ Even n) := even_mul
   _ ↔ Even n            := by simp

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

-- variable (a b : Prop)
-- variable (m : ℤ)
-- #check (even_mul : Even (m * n) ↔ Even m ∨ Even n)
-- #check (iff_of_eq : a = b → (a ↔ b))
-- #check (odd_iff_not_even : Odd n ↔ ¬Even n)
-- #check (or_self_iff a : a ∨ a ↔ a)

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

1.3. Demostraciones con Isabelle/HOL

theory Un_numero_es_par_syss_lo_es_su_cuadrado
imports Main
begin

(* 1ª demostración *)

lemma
  fixes n :: int
  shows "even (n⇧2) ⟷ even n"
proof (rule iffI)
  assume "even (n⇧2)"
  show "even n"
  proof (rule ccontr)
    assume "odd n"
    then obtain k where "n = 2*k+1"
      by (rule oddE)
    then have "n⇧2 = 2*(2*k*(k+1))+1"
    proof -
      have "n⇧2 = (2*k+1)⇧2"
        by (simp add: ‹n = 2 * k + 1›)
      also have "… = 4*k⇧2+4*k+1"
        by algebra
      also have "… = 2*(2*k*(k+1))+1"
        by algebra
      finally show "n⇧2 = 2*(2*k*(k+1))+1" .
    qed
    then have "∃k'. n⇧2 = 2*k'+1"
      by (rule exI)
    then have "odd (n⇧2)"
      by fastforce
    then show False
      using ‹even (n⇧2)› by blast
  qed
next
  assume "even n"
  then obtain k where "n = 2*k"
    by (rule evenE)
  then have "n⇧2 = 2*(2*k⇧2)"
    by simp
  then show "even (n⇧2)"
    by simp
qed

(* 2ª demostración *)

lemma
  fixes n :: int
  shows "even (n⇧2) ⟷ even n"
proof
  assume "even (n⇧2)"
  show "even n"
  proof (rule ccontr)
    assume "odd n"
    then obtain k where "n = 2*k+1"
      by (rule oddE)
    then have "n⇧2 = 2*(2*k*(k+1))+1"
      by algebra
    then have "odd (n⇧2)"
      by simp
    then show False
      using ‹even (n⇧2)› by blast
  qed
next
  assume "even n"
  then obtain k where "n = 2*k"
    by (rule evenE)
  then have "n⇧2 = 2*(2*k⇧2)"
    by simp
  then show "even (n⇧2)"
    by simp
qed

(* 3ª demostración *)

lemma
  fixes n :: int
  shows "even (n⇧2) ⟷ even n"
proof -
  have "even (n⇧2) = (even n ∧ (0::nat) < 2)"
    by (simp only: even_power)
  also have "… = (even n ∧ True)"
    by (simp only: less_numeral_simps)
  also have "… = even n"
    by (simp only: HOL.simp_thms(21))
  finally show "even (n⇧2) ⟷ even n"
    by this
qed

(* 4ª demostración *)

lemma
  fixes n :: int
  shows "even (n⇧2) ⟷ even n"
proof -
  have "even (n⇧2) = (even n ∧ (0::nat) < 2)"
    by (simp only: even_power)
  also have "… = even n"
    by simp
  finally show "even (n⇧2) ⟷ even n" .
qed

(* 5ª demostración *)

lemma
  fixes n :: int
  shows "even (n⇧2) ⟷ even n"
  by simp

end

2. Las sucesiones convergentes están acotadas

Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir, \[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]

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

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

variable {u : ℕ → ℝ}

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

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by sorry

2.1. Demostración en lenguaje natural

Puesto que la sucesión \(u_n\) es convergente, existe un \(a ∈ ℝ\) tal que \[ \lim(u_n) = a \] Luego, existe un \(k ∈ ℕ\) tal que \[ (∀ n ∈ ℕ)[n ≥ k → |u_n - a | < 1] \tag{1} \] Veamos que \[ (∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ 1 + |a]] \] Para ello, sea \(n ∈ ℕ\) tal que \[ n ≥ k \tag{2} \] Entonces, \begin{align} |u_n| &= |u_n - a + a| \newline &≤ |u_n - a| + |a| \newline &≤ 1 + |a| &&\text{[por (1) y (2)]} \end{align}

2.2. Demostraciones con Lean4

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

variable {u : ℕ → ℝ}

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

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

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

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by
  cases' h with a ua
  -- a : ℝ
  -- ua : limite u a
  cases' ua 1 zero_lt_one with k h
  -- k : ℕ
  -- h : ∀ (n : ℕ), n ≥ k → |u n - a| ≤ 1
  use k, 1 + |a|
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n| ≤ 1 + |a|
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n| ≤ 1 + |a|
  specialize h n hn
  -- ⊢ |u n| ≤ 1 + |a|
  calc |u n|
       = |u n - a + a|   := congr_arg abs (eq_add_of_sub_eq rfl)
     _ ≤ |u n - a| + |a| := abs_add (u n - a) a
     _ ≤ 1 + |a|         := add_le_add_right h |a|

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

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by
  cases' h with a ua
  -- a : ℝ
  -- ua : limite u a
  cases' ua 1 zero_lt_one with k h
  -- k : ℕ
  -- h : ∀ (n : ℕ), n ≥ k → |u n - a| ≤ 1
  use k, 1 + |a|
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n| ≤ 1 + |a|
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n| ≤ 1 + |a|
  specialize h n hn
  -- h : |u n - a| ≤ 1
  calc |u n|
       = |u n - a + a|   := by ring_nf
     _ ≤ |u n - a| + |a| := abs_add (u n - a) a
     _ ≤ 1 + |a|         := by linarith

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

-- variable (a b c : ℝ)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (add_le_add_right : b ≤ c → ∀ a,  b + a ≤ c + a)
-- #check (eq_add_of_sub_eq :  a - c = b → a = b + c)
-- #check (zero_lt_one : 0 < 1)

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

2.3. Demostraciones con Isabelle/HOL

theory Acotacion_de_convergentes
imports Main HOL.Real
begin

(* (limite u c) expresa que el límite de u es c. *)
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (convergente u) expresa que u es convergente. *)
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"

(* 1ª demostración *)

lemma
  assumes "convergente u"
  shows   "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
proof -
  obtain a where "limite u a"
    using assms convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"
    using limite_def zero_less_one by blast
  have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"
  proof (intro allI impI)
    fix n
    assume hn : "n ≥ k"
    have "¦u n¦ = ¦u n - a + a¦"     by simp
    also have "… ≤ ¦u n - a¦ + ¦a¦" by simp
    also have "… ≤ 1 + ¦a¦"         by (simp add: hk hn)
    finally show "¦u n¦ ≤ 1 + ¦a¦"  .
  qed
  then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
    by (intro exI)
qed

end

3. La paradoja del barbero

Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.

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

import Mathlib.Tactic

variable (Hombre : Type)
variable (afeita : Hombre → Hombre → Prop)

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
by sorry

3.1. Demostración en lenguaje natural

Tenemos que demostrar que \[ ¬((∃ x)(∀ y)[\text{afeita}(x,y) ↔ ¬\text{afeita}(y,y)]) \] Para ello, supongamos que \[ (∃ x)(∀ y)[\text{afeita}(x,y) ↔ ¬\text{afeita}(y,y)] \tag{1} \] y tenemos que llegar a una contradicción.

Sea \(b\) un elemento que verifica (1); es decir, \[ (∀ y)[\text{afeita}(b,y) ↔ ¬\text{afeita}(y,y)] \] Entonces, \[ \text{afeita}(b,b) ↔ ¬\text{afeita}(b,b) \] que es una contradicción.

3.2. Demostraciones con Lean4

import Mathlib.Tactic

variable (Hombre : Type)
variable (afeita : Hombre → Hombre → Prop)

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

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
by
  intro h
  -- h : ∃ x, ∀ (y : Hombre), afeita x y ↔ ¬afeita y y
  -- ⊢ False
  cases' h with b hb
  -- b : Hombre
  -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y
  specialize hb b
  -- hb : afeita b b ↔ ¬afeita b b
  by_cases (afeita b b)
  . -- h : afeita b b
    apply absurd h
    -- ⊢ ¬afeita b b
    exact hb.mp h
  . -- h : ¬afeita b b
    apply h
    -- ⊢ afeita b b
    exact hb.mpr h

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

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
by
  intro h
  -- h : ∃ x, ∀ (y : Hombre), afeita x y ↔ ¬afeita y y
  -- ⊢ False
  cases' h with b hb
  -- b : Hombre
  -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y
  specialize hb b
  -- hb : afeita b b ↔ ¬afeita b b
  by_cases (afeita b b)
  . -- h : afeita b b
    exact (hb.mp h) h
  . -- h : ¬afeita b b
    exact h (hb.mpr h)

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

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
by
  intro h
  -- h : ∃ x, ∀ (y : Hombre), afeita x y ↔ ¬afeita y y
  -- ⊢ False
  cases' h with b hb
  -- b : Hombre
  -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y
  exact iff_not_self (hb b)

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

example :
  ¬ (∃ x : Hombre,  ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) :=
by
  rintro ⟨b, hb⟩
  -- b : Hombre
  -- hb : ∀ (y : Hombre), afeita b y ↔ ¬afeita y y
  -- ⊢ False
  exact iff_not_self (hb b)

-- 5ª demostración
-- ===============

example :
  ¬ (∃ x : Hombre,  ∀ y : Hombre, afeita x y ↔ ¬ afeita y y ) :=
fun ⟨b, hb⟩ ↦ iff_not_self (hb b)

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

-- variable (p q : Prop)
-- #check (absurd : p → (¬p → q))
-- #check (iff_not_self : ¬(p ↔ ¬p))

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

3.3. Demostraciones con Isabelle/HOL

theory La_paradoja_del_barbero
imports Main
begin

(* 1ª demostración *)

lemma
  "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"
proof (rule notI)
  assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y"
  then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y"
    by (rule exE)
  then have h : "afeita b b ⟷ ¬ afeita b b"
    by (rule allE)
  show False
  proof (cases "afeita b b")
    assume "afeita b b"
    then have "¬ afeita b b"
      using h by (rule rev_iffD1)
    then show False
      using ‹afeita b b› by (rule notE)
  next
    assume "¬ afeita b b"
    then have "afeita b b"
      using h by (rule rev_iffD2)
    with ‹¬ afeita b b› show False
      by (rule notE)
  qed
qed

(* 2ª demostración *)

lemma
  "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"
proof
  assume "∃ x. ∀ y. afeita x y ⟷ ¬ afeita y y"
  then obtain b where "∀ y. afeita b y ⟷ ¬ afeita y y"
    by (rule exE)
  then have h : "afeita b b ⟷ ¬ afeita b b"
    by (rule allE)
  then show False
    by simp
qed

(* 3ª demostración *)

lemma
  "¬(∃ x::'H. ∀ y::'H. afeita x y ⟷ ¬ afeita y y)"
  by auto

end

4. Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y

Demostrar con Lean4 que si \(x, y ∈ ℝ\) tales que \((∀ z)[y < z → x ≤ z]\), entonces \(x ≤ y\).

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

import Mathlib.Data.Real.Basic

variable {x y : ℝ}

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by sorry

4.1. Demostración en lenguaje natural

Lo demostraremos por reducción al absurdo. Para ello, supongamos que \[ x ≰ y \] Entonces \[ y < x \] y, por la densidad de \(ℝ\), existe un \(a\) tal que \[ y < a < x \] Puesto que \(y < a\), por la hipótesis, se tiene que \[ x ≤ a \] en contradicción con \[ a < x \]

4.2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable {x y : ℝ}

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

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by
  by_contra h1
  -- h1 : ¬x ≤ y
  -- ⊢ False
  have hxy : x > y := not_le.mp h1
  -- ⊢ ¬x > y
  cases' (exists_between hxy) with a ha
  -- a : ℝ
  -- ha : y < a ∧ a < x
  apply (lt_irrefl a)
  -- ⊢ a < a
  calc a
       < x := ha.2
     _ ≤ a := h a ha.1

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

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by
  apply le_of_not_gt
  -- ⊢ ¬x > y
  intro hxy
  -- hxy : x > y
  -- ⊢ False
  cases' (exists_between hxy) with a ha
  -- a : ℝ
  -- ha : y < a ∧ a < x
  apply (lt_irrefl a)
  -- ⊢ a < a
  calc a
       < x := ha.2
     _ ≤ a := h a ha.1

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

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by
  apply le_of_not_gt
  -- ⊢ ¬x > y
  intro hxy
  -- hxy : x > y
  -- ⊢ False
  cases' (exists_between hxy) with a ha
  -- ha : y < a ∧ a < x
  apply (lt_irrefl a)
  -- ⊢ a < a
  exact lt_of_lt_of_le ha.2 (h a ha.1)

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

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by
  apply le_of_not_gt
  -- ⊢ ¬x > y
  intro hxy
  -- hxy : x > y
  -- ⊢ False
  cases' (exists_between hxy) with a ha
  -- a : ℝ
  -- ha : y < a ∧ a < x
  exact (lt_irrefl a) (lt_of_lt_of_le ha.2 (h a ha.1))

-- 5ª demostración
-- ===============

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
by
  apply le_of_not_gt
  -- ⊢ ¬x > y
  intro hxy
  -- hxy : x > y
  -- ⊢ False
  rcases (exists_between hxy) with ⟨a, hya, hax⟩
  -- a : ℝ
  -- hya : y < a
  -- hax : a < x
  exact (lt_irrefl a) (lt_of_lt_of_le hax (h a hya))

-- 6ª demostración
-- ===============

example
  (h : ∀ z, y < z → x ≤ z) :
  x ≤ y :=
le_of_forall_le_of_dense h

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

-- variable (z : ℝ)
-- #check (exists_between : x < y → ∃ z, x < z ∧ z < y)
-- #check (le_of_forall_le_of_dense : (∀ z, y < z → x ≤ z) → x ≤ y)
-- #check (le_of_not_gt : ¬x > y → x ≤ y)
-- #check (lt_irrefl x : ¬x < x)
-- #check (lt_of_lt_of_le : x < y → y ≤ z → x < z)
-- #check (not_le : ¬x ≤ y ↔ y < x)

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

4.3. Demostraciones con Isabelle/HOL

theory Propiedad_de_la_densidad_de_los_reales
imports Main HOL.Real
begin

(* 1ª demostración *)

lemma
  fixes x y :: real
  assumes "∀ z. y < z ⟶ x ≤ z"
  shows "x ≤ y"
proof (rule linorder_class.leI; intro notI)
  assume "y < x"
  then have "∃z. y < z ∧ z < x"
    by (rule dense)
  then obtain a where ha : "y < a ∧ a < x"
    by (rule exE)
  have "¬ a < a"
    by (rule order.irrefl)
  moreover
  have "a < a"
  proof -
    have "y < a ⟶ x ≤ a"
      using assms by (rule allE)
    moreover
    have "y < a"
      using ha by (rule conjunct1)
    ultimately have "x ≤ a"
      by (rule mp)
    moreover
    have "a < x"
      using ha by (rule conjunct2)
    ultimately show "a < a"
      by (simp only: less_le_trans)
  qed
  ultimately show False
    by (rule notE)
qed

(* 2ª demostración *)

lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
proof (rule linorder_class.leI; intro notI)
  assume "y < x"
  then have "∃z. y < z ∧ z < x"
    by (rule dense)
  then obtain a where hya : "y < a" and hax : "a < x"
    by auto
  have "¬ a < a"
    by (rule order.irrefl)
  moreover
  have "a < a"
  proof -
    have "a < x"
      using hax .
    also have "… ≤ a"
      using assms[OF hya] .
    finally show "a < a" .
  qed
  ultimately show False
    by (rule notE)
qed

(* 3ª demostración *)

lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
proof (rule linorder_class.leI; intro notI)
  assume "y < x"
  then have "∃z. y < z ∧ z < x"
    by (rule dense)
  then obtain a where hya : "y < a" and hax : "a < x"
    by auto
  have "¬ a < a"
    by (rule order.irrefl)
  moreover
  have "a < a"
    using hax assms[OF hya] by (rule less_le_trans)
  ultimately show False
    by (rule notE)
qed

(* 4ª demostración *)

lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
by (meson assms dense not_less)

(* 5ª demostración *)

lemma
  fixes x y :: real
  assumes "⋀ z. y < z ⟹ x ≤ z"
  shows "x ≤ y"
using assms by (rule dense_ge)

(* 6ª demostración *)

lemma
  fixes x y :: real
  assumes "∀ z. y < z ⟶ x ≤ z"
  shows "x ≤ y"
using assms by (simp only: dense_ge)

end

5. Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ

En Lean4, una sucesión \(u_0, u_1, u_2, \dots\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el \(n\)-ésimo término de la sucesión.

Se define que \(a\) límite de la sucesión \(u\) como sigue

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

Demostrar que si \((∀ n)[u_n ≤ v_n]\), \(a\) es límite de \(u_n\) y \(c\) es límite de \(v_n\), entonces \(a ≤ c\).

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

import Mathlib.Data.Real.Basic

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

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

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by sorry

5.1. Demostración en lenguaje natural

Por reduccion al absurdo. Supongamos que \(a ≰ c\). Entonces, \[ c < a \tag{1} \] Sea \[ ε = \frac{a - c}{2} \tag{2} \] Por (1), \[ ε > 0 \] Por tanto, puesto que \(a\) es límite de \(u_n\), existe un \(p ∈ ℕ\) tal que \[ (∀ n)[n ≥ p → |u_n - a| < ε] \tag{3} \] Análogamente, puesto que c es límite de \(v_n\), existe un \(q ∈ ℕ\) tal que \[ (∀ n)[n ≥ q → |v_n - c| < ε] \tag{4} \] Sea \[ k = \max(p, q) \] Entonces, \(k ≥ p\) y, por (3), \[ |u_k - a| < ε \tag{5} \] Análogamente, \(k ≥ q\) y, por (4), \[ |v_k - c| < ε \tag{6} \] Además, por la hipótesis, \[ u_k ≤ v_k \tag{7} \] Por tanto, \begin{align} a - c &= (a - u_k) + (u_k - c) \newline &≤ (a - u_k) + (v_k - c) &&\text{[por (7)]} \newline &≤ |(a - u_k) + (v_k - c)| \newline &≤ |a - u_k| + |v_k - c| \newline &= |u_k - a| + |v_k - c| \newline &< ε + ε &&\text{[por (5) y (6)]} \newline &= a - c &&\text{[por (2)]} \end{align} Luego, \[ a - c < a - c \] que es una contradicción.

5.2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic

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

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

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

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by
  by_contra h
  -- h : ¬a ≤ c
  -- ⊢ False
  have hca : c < a := not_le.mp h
  set ε := (a - c) /2
  have hε : 0 < ε := half_pos (sub_pos.mpr hca)
  obtain ⟨ku, hku : ∀ n, n ≥ ku → |u n - a| < ε⟩ := hu ε hε
  obtain ⟨kv, hkv : ∀ n, n ≥ kv → |v n - c| < ε⟩ := hv ε hε
  let k := max ku kv
  have hku' : ku ≤ k := le_max_left ku kv
  have hkv' : kv ≤ k := le_max_right ku kv
  have ha : |u k - a| < ε := hku k hku'
  have hc : |v k - c| < ε := hkv k hkv'
  have hk : u k - c ≤ v k - c := sub_le_sub_right (huv k) c
  have hac1 : a - c < a - c := by
    calc a - c
         = (a - u k) + (u k - c)   := by ring
       _ ≤ (a - u k) + (v k - c)   := add_le_add_left hk (a - u k)
       _ ≤ |(a - u k) + (v k - c)| := le_abs_self ((a - u k) + (v k - c))
       _ ≤ |a - u k| + |v k - c|   := abs_add (a - u k) (v k - c)
       _ = |u k - a| + |v k - c|   := by simp only [abs_sub_comm]
       _ < ε + ε                   := add_lt_add ha hc
       _ = a - c                   := add_halves (a - c)
  have hac2 : ¬ a - c < a -c := lt_irrefl (a - c)
  show False
  exact hac2 hac1

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

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by
  by_contra h
  -- h : ¬a ≤ c
  -- ⊢ False
  have hca : c < a := not_le.mp h
  set ε := (a - c) /2 with hε
  obtain ⟨ku, hku : ∀ n, n ≥ ku → |u n - a| < ε⟩ := hu ε (by linarith)
  obtain ⟨kv, hkv : ∀ n, n ≥ kv → |v n - c| < ε⟩ := hv ε (by linarith)
  let k := max ku kv
  have ha : |u k - a| < ε := hku k (le_max_left ku kv)
  have hc : |v k - c| < ε := hkv k (le_max_right ku kv)
  have hk : u k - c ≤ v k - c := sub_le_sub_right (huv k) c
  have hac1 : a - c < a -c := by
    calc a - c
         = (a - u k) + (u k - c)   := by ring
       _ ≤ (a - u k) + (v k - c)   := add_le_add_left hk (a - u k)
       _ ≤ |(a - u k) + (v k - c)| := le_abs_self ((a - u k) + (v k - c))
       _ ≤ |a - u k| + |v k - c|   := abs_add (a - u k) (v k - c)
       _ = |u k - a| + |v k - c|   := by simp only [abs_sub_comm]
       _ < ε + ε                   := add_lt_add ha hc
       _ = a - c                   := add_halves (a - c)
  have hac2 : ¬ a - c < a -c := lt_irrefl (a - c)
  show False
  exact hac2 hac1

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

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by
  by_contra h
  -- h : ¬a ≤ c
  -- ⊢ False
  have hca : c < a := not_le.mp h
  set ε := (a - c) /2 with hε
  obtain ⟨ku, hku : ∀ n, n ≥ ku → |u n - a| < ε⟩ := hu ε (by linarith)
  obtain ⟨kv, hkv : ∀ n, n ≥ kv → |v n - c| < ε⟩ := hv ε (by linarith)
  let k := max ku kv
  have ha : |u k - a| < ε := hku k (le_max_left ku kv)
  have hc : |v k - c| < ε := hkv k (le_max_right ku kv)
  have hk : u k - c ≤ v k - c := sub_le_sub_right (huv k) c
  have hac1 : a - c < a -c := by
    calc a - c
         = (a - u k) + (u k - c)   := by ring
       _ ≤ (a - u k) + (v k - c)   := add_le_add_left hk (a - u k)
       _ ≤ |(a - u k) + (v k - c)| := by simp [le_abs_self]
       _ ≤ |a - u k| + |v k - c|   := by simp [abs_add]
       _ = |u k - a| + |v k - c|   := by simp [abs_sub_comm]
       _ < ε + ε                   := add_lt_add ha hc
       _ = a - c                   := by simp
  have hac2 : ¬ a - c < a -c := lt_irrefl (a - c)
  show False
  exact hac2 hac1

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

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by
  apply le_of_not_lt
  -- ⊢ ¬c < a
  intro hca
  -- hca : c < a
  -- ⊢ False
  set ε := (a - c) /2 with hε
  cases' hu ε (by linarith) with ku hku
  -- ku : ℕ
  -- hku : ∀ (n : ℕ), n ≥ ku → |u n - a| < ε
  cases' hv ε (by linarith) with kv hkv
  -- kv : ℕ
  -- hkv : ∀ (n : ℕ), n ≥ kv → |v n - c| < ε
  let k := max ku kv
  have ha : |u k - a| < ε := hku k (le_max_left ku kv)
  have hc : |v k - c| < ε := hkv k (le_max_right ku kv)
  have hk : u k ≤ v k := huv k
  apply lt_irrefl (a - c)
  -- ⊢ a - c < a - c
  rw [abs_lt] at ha hc
  -- ha : -ε < u k - a ∧ u k - a < ε
  -- hc : -ε < v k - c ∧ v k - c < ε
  linarith

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

-- variable (b d : ℝ)
-- #check (abs_add a b : |a + b| ≤ |a| + |b|)
-- #check (abs_lt: |a| < b ↔ -b < a ∧ a < b)
-- #check (abs_sub_comm a b : |a - b| = |b - a|)
-- #check (add_halves a : a / 2 + a / 2 = a)
-- #check (add_le_add_left : b ≤ c → ∀ a, a + b ≤ a + c)
-- #check (add_lt_add : a < b → c < d → a + c < b + d)
-- #check (half_pos : 0 < a → 0 < a / 2)
-- #check (le_abs_self a : a ≤ |a|)
-- #check (le_max_left a b : a ≤ max a b)
-- #check (le_max_right a b : b ≤ max a b)
-- #check (le_of_not_lt :  ¬b < a → a ≤ b)
-- #check (lt_irrefl a : ¬a < a)
-- #check (not_le : ¬a ≤ b ↔ b < a)
-- #check (sub_le_sub_right : a ≤ b → ∀ c, a - c ≤ b - c)
-- #check (sub_pos : 0 < a - b ↔ b < a)

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

5.3. Demostraciones con Isabelle/HOL

theory Limite_de_sucesion_menor_que_otra_sucesion
imports Main HOL.Real
begin

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

(* 1ª demostración *)

lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  have "a - c < a - c"
  proof -
    have "a - c = (a - u ?N) + (u ?N - c)"
      by simp
    also have "… ≤ (a - u ?N) + (v ?N - c)"
      using assms(3) by auto
    also have "… ≤ ¦(a - u ?N) + (v ?N - c)¦"
      by (rule abs_ge_self)
    also have "… ≤ ¦a - u ?N¦ + ¦v ?N - c¦"
      by (rule abs_triangle_ineq)
    also have "… = ¦u ?N - a¦ + ¦v ?N - c¦"
      by (simp only: abs_minus_commute)
    also have "… < ?ε + ?ε"
      using Ha Hc by (simp only: add_strict_mono)
    also have "… = a - c"
      by (rule field_sum_of_halves)
    finally show "a - c < a - c"
      by this
  qed
  have "¬ a - c < a - c"
    by (rule less_irrefl)
  then show False
    using ‹a - c < a - c› by (rule notE)
qed

(* 2ª demostración *)

lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"
    by argo
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"
    by argo
  have "a - c < a - c"
    using assms(3) Ha' Hc'
    by (smt (verit, best) field_sum_of_halves)
  have "¬ a - c < a - c"
    by simp
  then show False
    using ‹a - c < a - c› by simp
qed

(* 3ª demostración *)

lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"
    by argo
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"
    by argo
  show False
    using assms(3) Ha' Hc'
    by (smt (verit, best) field_sum_of_halves)
qed

end