Ir al contenido principal

La semana en Calculemus (25 de mayo de 2024)

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

A continuación se muestran las soluciones.

1. Los monoides booleanos son conmutativos

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide \(M\) es booleano si \[ (∀ x ∈ M)[x·x = 1] \] y es conmutativo si \[ (∀ x, y ∈ M)[x·y = y·x] \]

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

Demostrar con Lean4 que los monoides booleanos son conmutativos.

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

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by sorry

1.1. Demostración en lenguaje natural

Sean \(a, b ∈ M\). Se verifica la siguiente cadena de igualdades \begin{align} a·b &= (a·b)·1 &&\text{[por mul_one]} \newline &= (a·b)·(a·a) &&\text{[por hipótesis, \(a·a = 1\)]} \newline &= ((a·b)·a)·a &&\text{[por mul_assoc]} \newline &= (a·(b·a))·a &&\text{[por mul_assoc]} \newline &= (1·(a·(b·a)))·a &&\text{[por one_mul]} \newline &= ((b·b)·(a·(b·a)))·a &&\text{[por hipótesis, \(b·b = 1\)]} \newline &= (b·(b·(a·(b·a))))·a &&\text{[por mul_assoc]} \newline &= (b·((b·a)·(b·a)))·a &&\text{[por mul_assoc]} \newline &= (b·1)·a &&\text{[por hipótesis, \((b·a)·(b·a) = 1\)]} \newline &= b·a &&\text{[por mul_one]} \end{align}

1.2. Demostraciones con Lean4

import Mathlib.Algebra.Group.Basic

variable {M : Type} [Monoid M]

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by
  intros a b
  calc a * b
       = (a * b) * 1
         := (mul_one (a * b)).symm
     _ = (a * b) * (a * a)
         := congrArg ((a*b) * .) (h a).symm
     _ = ((a * b) * a) * a
         := (mul_assoc (a*b) a a).symm
     _ = (a * (b * a)) * a
         := congrArg (. * a) (mul_assoc a b a)
     _ = (1 * (a * (b * a))) * a
         := congrArg (. * a) (one_mul (a*(b*a))).symm
     _ = ((b * b) * (a * (b * a))) * a
         := congrArg (. * a) (congrArg (. * (a*(b*a))) (h b).symm)
     _ = (b * (b * (a * (b * a)))) * a
         := congrArg (. * a) (mul_assoc b b (a*(b*a)))
     _ = (b * ((b * a) * (b * a))) * a
         := congrArg (. * a) (congrArg (b * .) (mul_assoc b a (b*a)).symm)
     _ = (b * 1) * a
         := congrArg (. * a) (congrArg (b * .) (h (b*a)))
     _ = b * a
         := congrArg (. * a) (mul_one b)

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by
  intros a b
  calc a * b
       = (a * b) * 1                   := by simp only [mul_one]
     _ = (a * b) * (a * a)             := by simp only [h a]
     _ = ((a * b) * a) * a             := by simp only [mul_assoc]
     _ = (a * (b * a)) * a             := by simp only [mul_assoc]
     _ = (1 * (a * (b * a))) * a       := by simp only [one_mul]
     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]
     _ = (b * (b * (a * (b * a)))) * a := by simp only [mul_assoc]
     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]
     _ = (b * 1) * a                   := by simp only [h (b*a)]
     _ = b * a                         := by simp only [mul_one]

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by
  intros a b
  calc a * b
       = (a * b) * 1                   := by simp only [mul_one]
     _ = (a * b) * (a * a)             := by simp only [h a]
     _ = (a * (b * a)) * a             := by simp only [mul_assoc]
     _ = (1 * (a * (b * a))) * a       := by simp only [one_mul]
     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]
     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]
     _ = (b * 1) * a                   := by simp only [h (b*a)]
     _ = b * a                         := by simp only [mul_one]

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
by
  intros a b
  calc a * b
       = (a * b) * 1                   := by simp
     _ = (a * b) * (a * a)             := by simp only [h a]
     _ = (a * (b * a)) * a             := by simp only [mul_assoc]
     _ = (1 * (a * (b * a))) * a       := by simp
     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]
     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]
     _ = (b * 1) * a                   := by simp only [h (b*a)]
     _ = b * a                         := by simp

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

-- variable (a b c : M)
-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))
-- #check (mul_one a : a * 1 = a)
-- #check (one_mul a : 1 * a = a)

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

1.3. Demostraciones con Isabelle/HOL

theory Los_monoides_booleanos_son_conmutativos
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * 1"
    by (simp only: right_neutral)
  also have "… = (a * b) * (a * a)"
    by (simp only: assms)
  also have "… = ((a * b) * a) * a"
    by (simp only: assoc)
  also have "… = (a * (b * a)) * a"
    by (simp only: assoc)
  also have "… = (1 * (a * (b * a))) * a"
    by (simp only: left_neutral)
  also have "… = ((b * b) * (a * (b * a))) * a"
    by (simp only: assms)
  also have "… = (b * (b * (a * (b * a)))) * a"
    by (simp only: assoc)
  also have "… = (b * ((b * a) * (b * a))) * a"
    by (simp only: assoc)
  also have "… = (b * 1) * a"
    by (simp only: assms)
  also have "… = b * a"
    by (simp only: right_neutral)
  finally show "a * b = b * a"
    by this
qed

(* 2ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * 1"                    by simp
  also have "… = (a * b) * (a * a)"             by (simp add: assms)
  also have "… = ((a * b) * a) * a"             by (simp add: assoc)
  also have "… = (a * (b * a)) * a"             by (simp add: assoc)
  also have "… = (1 * (a * (b * a))) * a"       by simp
  also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)
  also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc)
  also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)
  also have "… = (b * 1) * a"                   by (simp add: assms)
  also have "… = b * a"                         by simp
  finally show "a * b = b * a"                  by this
qed

(* 3ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * (a * a)"              by (simp add: assms)
  also have "… = (a * (b * a)) * a"             by (simp add: assoc)
  also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)
  also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)
  also have "… = (b * 1) * a"                   by (simp add: assms)
  finally show "a * b = b * a"                  by simp
qed

(* 4ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
  by (metis assms assoc right_neutral)

end

end

2. La composición de una función creciente y una decreciente es decreciente

Sea una función \(f\) de \(ℝ\) en \(ℝ\). Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\). Se dice que \(f\) es decreciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≥ f(y)\).

Demostrar con Lean4 que si \(f\) es creciente y \(g\) es decreciente, entonces \(g ∘ f\) es decreciente.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=
  ∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=
  ∀ {x y}, x ≤ y → f x ≥ f y

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by sorry

2.1. Demostración en lenguaje natural

Sean \(x, y ∈ ℝ\) tales que \(x ≤ y\). Entonces, por ser \(f\) creciente, \[ f(x) ≥ f(y) \] y, por ser g decreciente, \[ g(f(x)) ≤ g(f(y)) \] Por tanto, \[ (g ∘ f)(x) ≤ (g ∘ f)(y) \]

2.2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=
  ∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=
  ∀ {x y}, x ≤ y → f x ≥ f y

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

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  intro x y h
  -- x y : ℝ
  -- h : x ≤ y
  -- ⊢ (g ∘ f) x ≥ (g ∘ f) y
  have h1 : f x ≤ f y := hf h
  show (g ∘ f) x ≥ (g ∘ f) y
  exact hg h1

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

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  intro x y h
  -- x y : ℝ
  -- h : x ≤ y
  -- ⊢ (g ∘ f) x ≥ (g ∘ f) y
  show (g ∘ f) x ≥ (g ∘ f) y
  exact hg (hf h)

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

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
fun {_ _} h ↦ hg (hf h)

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

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  intros x y hxy
  calc (g ∘ f) x
       = g (f x)   := rfl
     _ ≥ g (f y)   := hg (hf hxy)
     _ = (g ∘ f) y := rfl

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

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  unfold creciente decreciente at *
  -- hf : ∀ {x y : ℝ}, x ≤ y → f x ≤ f y
  -- hg : ∀ {x y : ℝ}, x ≤ y → g x ≥ g y
  -- ⊢ ∀ {x y : ℝ}, x ≤ y → (g ∘ f) x ≥ (g ∘ f) y
  intros x y h
  -- x y : ℝ
  -- h : x ≤ y
  -- ⊢ (g ∘ f) x ≥ (g ∘ f) y
  unfold Function.comp
  -- ⊢ g (f x) ≥ g (f y)
  apply hg
  -- ⊢ f x ≤ f y
  apply hf
  -- ⊢ x ≤ y
  exact h

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

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  intros x y h
  -- x y : ℝ
  -- h : x ≤ y
  -- ⊢ (g ∘ f) x ≥ (g ∘ f) y
  apply hg
  -- ⊢ f x ≤ f y
  apply hf
  -- ⊢ x ≤ y
  exact h

-- 7ª demostración
-- ===============

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  intros x y h
  -- x y : ℝ
  -- h : x ≤ y
  -- ⊢ (g ∘ f) x ≥ (g ∘ f) y
  apply hg
  -- ⊢ f x ≤ f y
  exact hf h

-- 8ª demostración
-- ===============

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by
  intros x y h
  -- x y : ℝ
  -- h : x ≤ y
  -- ⊢ (g ∘ f) x ≥ (g ∘ f) y
  exact hg (hf h)

-- 9ª demostración
-- ===============

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
by tauto

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

2.3. Demostraciones con Isabelle/HOL

theory La_composicion_de_una_funcion_creciente_y_una_decreciente_es_decreciente
imports Main HOL.Real
begin

(* 1ª demostración *)

lemma
  fixes f g :: "real ⇒ real"
  assumes "mono f"
          "antimono g"
  shows   "antimono (g ∘ f)"
proof (rule antimonoI)
  fix x y :: real
  assume "x ≤ y"
  have "(g ∘ f) y = g (f y)"
    by (simp only: o_apply)
  also have "… ≤ g (f x)"
    using assms ‹x ≤ y›
    by (metis antimonoE monoD)
  also have "… = (g ∘ f) x"
    by (simp only: o_apply)
  finally show "(g ∘ f) x ≥ (g ∘ f) y"
    by this
qed

(* 2ª demostración *)

lemma
  fixes f g :: "real ⇒ real"
  assumes "mono f"
          "antimono g"
  shows   "antimono (g ∘ f)"
proof (rule antimonoI)
  fix x y :: real
  assume "x ≤ y"
  have "(g ∘ f) y = g (f y)"    by simp
  also have "… ≤ g (f x)"     by (meson ‹x ≤ y› assms antimonoE monoE)
  also have "… = (g ∘ f) x"    by simp
  finally show "(g ∘ f) x ≥ (g ∘ f) y" .
qed

(* 3ª demostración *)

lemma
  assumes "mono f"
          "antimono g"
  shows   "antimono (g ∘ f)"
  using assms(1) assms(2) monotone_on_o
  by blast

end

3. Si una función es creciente e involutiva, entonces es la identidad

Sea una función \(f\) de \(ℝ\) en \(ℝ\).

  • Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\).
  • Se dice que \(f\) es involutiva si para todo \(x\) se tiene que \(f(f(x)) = x\).

En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f

Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.

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

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

example
  (hc : Monotone f)
  (hi : Involutive f)
  : f = id :=
by sorry

3.1. Demostración en lenguaje natural

Tenemos que demostrar que para todo \(x ∈ ℝ\), \(f(x) = x\). Sea \(x ∈ ℝ\). Entonces, por ser \(f\) involutiva, se tiene que \[ f(f(x)) = x \tag{1} \] Además, por las propiedades del orden, se tiene que \(f(x) ≤ x\) ó \(x ≤ f(x)\). Demostraremos que \(f(x) = x\) en los dos casos.

Caso 1: Supongamos que \[ f(x) ≤ x \tag{2} \] Entonces, por ser \(f\) creciente, se tiene que \[ f(f(x)) ≤ f(x) \tag{3} \] Sustituyendo (1) en (3), se tiene \[ x ≤ f(x) \] que junto con (1) da \[ f(x) = x \]

Caso 2: Supongamos que \[ x ≤ f(x) \tag{4} \] Entonces, por ser \(f\) creciente, se tiene que \[ f(x) ≤ f(f(x)) \tag{5} \] Sustituyendo (1) en (5), se tiene \[ f(x) ≤ x \] que junto con (4) da \[ f(x) = x \]

3.2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

-- 1ª demostración
example
  (hc : Monotone f)
  (hi : Involutive f)
  : f = id :=
by
  funext x
  -- x : ℝ
  -- ⊢ f x = id x
  have h : f (f x) = x := hi x
  cases' (le_total (f x) x) with h1 h2
  . -- h1 : f x ≤ x
    have h1a : f (f x) ≤ f x := hc h1
    have h1b : x ≤ f x := by rwa [h] at h1a
    show f x = x
    exact antisymm h1 h1b
  . -- h2 : x ≤ f x
    have h2a : f x ≤ f (f x) := hc h2
    have h2b : f x ≤ x := by rwa [h] at h2a
    show f x = x
    exact antisymm h2b h2

-- 2ª demostración
example
  (hc : Monotone f)
  (hi : Involutive f)
  : f = id :=
by
  unfold Monotone Involutive at *
  -- hc : ∀ ⦃a b : ℝ⦄, a ≤ b → f a ≤ f b
  -- hi : ∀ (x : ℝ), f (f x) = x
  funext x
  -- x : ℝ
  -- ⊢ f x = id x
  unfold id
  -- ⊢ f x = x
  cases' (le_total (f x) x) with h1 h2
  . -- h1 : f x ≤ x
    apply antisymm h1
    -- ⊢ x ≤ f x
    have h3 : f (f x) ≤ f x := by
      apply hc
      -- ⊢ f x ≤ x
      exact h1
    rwa [hi] at h3
  . -- h2 : x ≤ f x
    apply antisymm _ h2
    -- ⊢ f x ≤ x
    have h4 : f x ≤ f (f x) := by
      apply hc
      -- ⊢ x ≤ f x
      exact h2
    rwa [hi] at h4

-- 3ª demostración
example
  (hc : Monotone f)
  (hi : Involutive f)
  : f = id :=
by
  funext x
  -- x : ℝ
  -- ⊢ f x = id x
  cases' (le_total (f x) x) with h1 h2
  . -- h1 : f x ≤ x
    apply antisymm h1
    -- ⊢ x ≤ f x
    have h3 : f (f x) ≤ f x := hc h1
    rwa [hi] at h3
  . -- h2 : x ≤ f x
    apply antisymm _ h2
    -- ⊢ f x ≤ x
    have h4 : f x ≤ f (f x) := hc h2
    rwa [hi] at h4

-- 4ª demostración
example
  (hc : Monotone f)
  (hi : Involutive f)
  : f = id :=
by
  funext x
  -- x : ℝ
  -- ⊢ f x = id x
  cases' (le_total (f x) x) with h1 h2
  . -- h1 : f x ≤ x
    apply antisymm h1
    -- ⊢ x ≤ f x
    calc x
         = f (f x) := (hi x).symm
       _ ≤ f x     := hc h1
  . -- h2 : x ≤ f x
    apply antisymm _ h2
    -- ⊢ f x ≤ x
    calc f x
         ≤ f (f x) := hc h2
       _ = x       := hi x

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

-- variable (a b : ℝ)
-- #check (le_total a b : a ≤ b ∨ b ≤ a)
-- #check (antisymm : a ≤ b → b ≤ a → a = b)

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

3.3. Demostraciones con Isabelle/HOL

theory Una_funcion_creciente_e_involutiva_es_la_identidad
imports Main HOL.Real
begin

definition involutiva :: "(real ⇒ real) ⇒ bool"
  where "involutiva f ⟷ (∀x. f (f x) = x)"

(* 1ª demostración *)

lemma
  fixes f :: "real ⇒ real"
  assumes "mono f"
          "involutiva f"
  shows   "f = id"
proof (unfold fun_eq_iff; intro allI)
  fix x
  have "x ≤ f x ∨ f x ≤ x"
    by (rule linear)
  then have "f x = x"
  proof (rule disjE)
    assume "x ≤ f x"
    then have "f x ≤ f (f x)"
      using assms(1) by (simp only: monoD)
    also have "… = x"
      using assms(2) by (simp only: involutiva_def)
    finally have "f x ≤ x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by (simp only: antisym)
  next
    assume "f x ≤ x"
    have "x = f (f x)"
      using assms(2) by (simp only: involutiva_def)
    also have "... ≤ f x"
      using ‹f x ≤ x› assms(1) by (simp only: monoD)
    finally have "x ≤ f x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by (simp only: monoD)
  qed
  then show "f x = id x"
    by (simp only: id_apply)
qed

(* 2ª demostración *)

lemma
  fixes f :: "real ⇒ real"
  assumes "mono f"
          "involutiva f"
  shows   "f = id"
proof
  fix x
  have "x ≤ f x ∨ f x ≤ x"
    by (rule linear)
  then have "f x = x"
  proof
    assume "x ≤ f x"
    then have "f x ≤ f (f x)"
      using assms(1) by (simp only: monoD)
    also have "… = x"
      using assms(2) by (simp only: involutiva_def)
    finally have "f x ≤ x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by auto
  next
    assume "f x ≤ x"
    have "x = f (f x)"
      using assms(2) by (simp only: involutiva_def)
    also have "... ≤ f x"
      by (simp add: ‹f x ≤ x› assms(1) monoD)
    finally have "x ≤ f x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by auto
  qed
  then show "f x = id x"
    by simp
qed

(* 3ª demostración *)

lemma
  fixes f :: "real ⇒ real"
  assumes "mono f"
          "involutiva f"
  shows   "f = id"
proof
  fix x
  have "x ≤ f x ∨ f x ≤ x"
    by (rule linear)
  then have "f x = x"
  proof
    assume "x ≤ f x"
    then have "f x ≤ x"
      by (metis assms involutiva_def mono_def)
    then show "f x = x"
      using ‹x ≤ f x› by auto
  next
    assume "f x ≤ x"
    then have "x ≤ f x"
      by (metis assms involutiva_def mono_def)
    then show "f x = x"
      using ‹f x ≤ x› by auto
  qed
  then show "f x = id x"
    by simp
qed

end

4. Si f(x) ≤ f(y) → x ≤ y, entonces f es inyectiva

Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que \[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \] entonces \(f\) es inyectiva.

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

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by sorry

4.1. Demostración en lenguaje natural

Sean \(x, y ∈ ℝ\) tales que \[ f(x) = f(y) \tag{1} \] Tenemos que demostrar que \(x = y\).

De (1), tenemos que \[ f(x) ≤ f(y) \] y, por la hipótesis, \[ x ≤ y \tag{2} \]

También de (1), tenemos que \[ f(y) ≤ f(x) \] y, por la hipótesis, \[ y ≤ x \tag{3} \]

De (2) y (3), tenemos que \[ x = y \]

4.2. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

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

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by
  intros x y hxy
  -- x y : ℝ
  -- hxy : f x = f y
  -- ⊢ x = y
  have h1 : f x ≤ f y := le_of_eq hxy
  have h2 : x ≤ y     := h h1
  have h3 : f y ≤ f x := ge_of_eq hxy
  have h4 : y ≤ x     := h h3
  show x = y
  exact le_antisymm h2 h4

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

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by
  intros x y hxy
  -- x y : ℝ
  -- hxy : f x = f y
  -- ⊢ x = y
  have h1 : x ≤ y     := h (le_of_eq hxy)
  have h2 : y ≤ x     := h (ge_of_eq hxy)
  show x = y
  exact le_antisymm h1 h2

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

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by
  intros x y hxy
  -- x y : ℝ
  -- hxy : f x = f y
  -- ⊢ x = y
  show x = y
  exact le_antisymm (h (le_of_eq hxy)) (h (ge_of_eq hxy))

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

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
fun _ _ hxy ↦ le_antisymm (h hxy.le) (h hxy.ge)

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

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by
  intros x y hxy
  -- x y : ℝ
  -- hxy : f x = f y
  -- ⊢ x = y
  apply le_antisymm
  . -- ⊢ x ≤ y
    apply h
    -- ⊢ f x ≤ f y
    exact le_of_eq hxy
  . -- ⊢ y ≤ x
    apply h
    -- ⊢ f y ≤ f x
    exact ge_of_eq hxy

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

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by
  intros x y hxy
  -- x y : ℝ
  -- hxy : f x = f y
  -- ⊢ x = y
  apply le_antisymm
  . -- ⊢ x ≤ y
    exact h (le_of_eq hxy)
  . -- ⊢ y ≤ x
    exact h (ge_of_eq hxy)

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

-- variable (a b : ℝ)
-- #check (ge_of_eq : a = b → a ≥ b)
-- #check (le_antisymm : a ≤ b → b ≤ a → a = b)
-- #check (le_of_eq : a = b → a ≤ b)

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

4.3. Demostraciones con Isabelle/HOL

theory "Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva"
imports Main HOL.Real
begin

(* 1ª demostración *)

lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  show "x = y"
  proof (rule antisym)
    show "x ≤ y"
      by (simp only: assms ‹f x = f y›)
  next
    show "y ≤ x"
      by (simp only: assms ‹f x = f y›)
  qed
qed

(* 2ª demostración *)

lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  then show "x = y"
    using assms
    by (simp add: eq_iff)
qed

(* 3ª demostración *)

lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
  by (simp add: assms injI eq_iff)
end

5. Los supremos de las sucesiones crecientes son sus límites

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

5.1. Demostración en lenguaje natural

Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que \[ (∃ m ∈ ℕ)(∀ n ∈ ℕ)[n ≥ m → |u_n - S| ≤ ε] \tag{1} \]

Por ser \(S\) un supremo de u, existe un k ∈ ℕ tal que \[ u_k ≥ S - ε \tag{2} \] Vamos a demostrar que \(k\) verifica la condición de (1); es decir, que si \(n ∈ ℕ\) tal que \(n ≥ k\), entonces \[ |u_n - S| ≤ ε \] o, equivalentemente, \[ -ε ≤ u_n - S ≤ ε \]

La primera desigualdad se tiene por la siguente cadena: \begin{align} -ε &= (S - ε) - S \newline &≤ u_k - S &&\text{[por (2)]} \newline &≤ u_n - S &&\text{[porque \(u\) es creciente y \(n ≥ k\)]} \end{align}

La segunda desigualdad se tiene por la siguente cadena: \begin{align} u_n - S &≤ S - S &&\text{[porque \(S\) es un supremo de \(u\)]} \newline &= 0 \newline &≤ ε \end{align}

5.2. Demostraciones con 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 - ε

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

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by
  unfold limite
  -- ⊢ ∀ (ε : ℝ), ε > 0 → ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε
  unfold supremo at hS
  -- hS : (∀ (n : ℕ), u n ≤ S) ∧ ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε
  cases' hS with hS₁ hS₂
  -- hS₁ : ∀ (n : ℕ), u n ≤ S
  -- hS₂ : ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε
  cases' hS₂ ε hε with k hk
  -- k : ℕ
  -- hk : u k ≥ S - ε
  use k
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n - S| ≤ ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n - S| ≤ ε
  rw [abs_le]
  -- ⊢ -ε ≤ u n - S ∧ u n - S ≤ ε
  constructor
  . -- ⊢ -ε ≤ u n - S
    unfold Monotone at hu
    -- hu : ∀ ⦃a b : ℕ⦄, a ≤ b → u a ≤ u b
    specialize hu hn
    -- hu : u k ≤ u n
    calc -ε
         = (S - ε) - S := by ring
       _ ≤ u k - S     := sub_le_sub_right hk S
       _ ≤ u n - S     := sub_le_sub_right hu S
  . calc u n - S
         ≤ S - S       := sub_le_sub_right (hS₁ n) S
       _ = 0           := sub_self S
       _ ≤ ε           := le_of_lt hε

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

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε
  cases' hS with hS₁ hS₂
  -- hS₁ : ∀ (n : ℕ), u n ≤ S
  -- hS₂ : ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε
  cases' hS₂ ε hε with k hk
  -- k : ℕ
  -- hk : u k ≥ S - ε
  use k
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n - S| ≤ ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n - S| ≤ ε
  rw [abs_le]
  -- ⊢ -ε ≤ u n - S ∧ u n - S ≤ ε
  constructor
  . -- ⊢ -ε ≤ u n - S
    linarith [hu hn]
  . -- ⊢ u n - S ≤ ε
    linarith [hS₁ n]

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

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ m, ∀ (n : ℕ), n ≥ m → |u n - S| ≤ ε
  cases' hS with hS₁ hS₂
  -- hS₁ : ∀ (n : ℕ), u n ≤ S
  -- hS₂ : ∀ (ε : ℝ), ε > 0 → ∃ k, u k ≥ S - ε
  cases' hS₂ ε hε with k hk
  -- k : ℕ
  -- hk : u k ≥ S - ε
  use k
  -- ⊢ ∀ (n : ℕ), n ≥ k → |u n - S| ≤ ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |u n - S| ≤ ε
  rw [abs_le]
  -- ⊢ -ε ≤ u n - S ∧ u n - S ≤ ε
  constructor <;> linarith [hu hn, hS₁ n]

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

-- variable (a b : ℝ)
-- #check (abs_le : |a| ≤ b ↔ -b ≤ a ∧ a ≤ b)
-- #check (le_of_lt : a < b → a ≤ b)
-- #check (sub_le_sub_right : a ≤ b → ∀ (c : ℝ), a - c ≤ b - c)
-- #check (sub_self a : a - a = 0)

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

5.3. Demostraciones con Isabelle/HOL

theory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites
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¦ ≤ ε)"

(* (supremo u M) expresa que el supremo de u es M. *)
definition supremo :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "supremo u M ⟷ ((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

(* 1ª demostración *)

lemma
  assumes "mono u"
          "supremo u M"
  shows   "limite u M"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"
    using assms(2)
    by (simp add: supremo_def)
  then have "∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε"
    by (rule conjunct2)
  then have "∃k. ∀n≥k. u n ≥ M - ε"
    by (simp only: ‹0 < ε›)
  then obtain n0 where "∀n≥n0. u n ≥ M - ε"
    by (rule exE)
  have "∀n≥n0. ¦u n - M¦ ≤ ε"
  proof (intro allI impI)
    fix n
    assume "n ≥ n0"
    show "¦u n - M¦ ≤ ε"
    proof (rule abs_leI)
      have "∀n. u n ≤ M"
        using hM by (rule conjunct1)
      then have "u n - M ≤ M - M"
        by simp
      also have "… = 0"
        by (simp only: diff_self)
      also have "… ≤ ε"
        using ‹0 < ε› by (simp only: less_imp_le)
      finally show "u n - M ≤ ε"
        by this
    next
      have "-ε = (M - ε) - M"
        by simp
      also have "… ≤ u n - M"
        using ‹∀n≥n0. M - ε ≤ u n› ‹n0 ≤ n› by auto
      finally have "-ε ≤ u n - M"
        by this
      then show "- (u n - M) ≤ ε"
        by simp
    qed
  qed
  then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"
    by (rule exI)
qed

(* 2ª demostración *)

lemma
  assumes "mono u"
          "supremo u M"
  shows   "limite u M"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"
    using assms(2)
    by (simp add: supremo_def)
  then have "∃k. ∀n≥k. u n ≥ M - ε"
    using ‹0 < ε› by presburger
  then obtain n0 where "∀n≥n0. u n ≥ M - ε"
    by (rule exE)
  then have "∀n≥n0. ¦u n - M¦ ≤ ε"
    using hM by auto
  then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"
    by (rule exI)
qed

end