Ir al contenido principal

La semana en Calculemus (8 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. Si uₙ está acotada y lim vₙ = 0, entonces lim (uₙ·vₙ) = 0

Demostrar con Lean4 que si \(u_n\) está acotada y \(lim v_n = 0\), entonces \(lim (u_n·v_n) = 0\).

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

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

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

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

def acotada (a : ℕ → ℝ) :=
  ∃ B, ∀ n, |a n| ≤ B

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
by sorry

1.1. Demostración en lenguaje natural

Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar \[ (∃ k)(∀ n)[n ≥ k → |(u·v)_n - 0| < ε] \tag{1} \]

Puesto que la sucesión \(u\) está acotada, existe un \(B ∈ ℝ\) tal que \[ (∀ n ∈ ℕ) |u_n| ≤ B \tag{2} \] Luego \(B ≥ 0\). Lo demostraremos por caso según que \(B = 0\) ó \(B > 0\).

Caso 1: Supongamos que \(B = 0\). Entonces, por (2), \[ (∀ n ∈ ℕ) |u_n| ≤ 0 \] Luego, \[ (∀ n ∈ ℕ) u_n = 0 \tag{3} \] Para demostrar (1), para basta tomar \(0\) como \(k\), ya que si \(n ≥ 0\), entonces \begin{align} |(u·v)_n - 0| &= |u_n·v_n| \newline &= |0·v_n| &&\text{[por (3)} \newline &= 0 \newline &< ε \w¡end{align}

Caso 2: Supongamos que \(B > 0\). Entonces, \(\dfrac{ε}{B} > 0\) y, puesto que \(lim v_n = 0\), existe un \(k ∈ ℕ\) tal que \[ (∀ n)[n ≥ k → |v_n - 0| < \dfrac{ε}{B}] \tag{4} \] Para demostrar (1), para basta el mismo \(k\), ya que si \(n ≥ k\), entonces \begin{align} |(u·v)_n - 0| &= |u_n·v_n| \newline &= |u_n|·|v_n| \newline &≤ B·|v_n| &&\text{[por (2)]} \newline &< B·\frac{ε}{B} &&\text{[por (4)]} \newline &= ε \end{align}

1.2. Demostraciones con Lean4

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

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

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

def acotada (a : ℕ → ℝ) :=
  ∃ B, ∀ n, |a n| ≤ B

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

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
by
  cases' hU with B hB
  -- B : ℝ
  -- hB : ∀ (n : ℕ), |u n| ≤ B
  have hBnoneg : 0 ≤ B :=
    calc 0 ≤ |u 0| := abs_nonneg (u 0)
         _ ≤ B     := hB 0
  by_cases hB0 : B = 0
  . -- hB0 : B = 0
    subst hB0
    -- hB : ∀ (n : ℕ), |u n| ≤ 0
    -- hBnoneg : 0 ≤ 0
    intros ε hε
    -- ε : ℝ
    -- hε : ε > 0
    -- ⊢ ∃ k, ∀ (n : ℕ), n ≥ k → |(u * v) n - 0| < ε
    use 0
    -- ⊢ ∀ (n : ℕ), n ≥ 0 → |(u * v) n - 0| < ε
    intros n _hn
    -- n : ℕ
    -- hn : n ≥ 0
    -- ⊢ |(u * v) n - 0| < ε
    simp_rw [sub_zero] at *
    -- ⊢ |(u * v) n| < ε
    calc |(u * v) n|
         = |u n * v n|   := congr_arg abs (Pi.mul_apply u v n)
       _ = |u n| * |v n| := abs_mul (u n) (v n)
       _ ≤ 0 * |v n|     := mul_le_mul_of_nonneg_right (hB n) (abs_nonneg (v n))
       _ = 0             := zero_mul (|v n|)
       _ < ε             := hε
  . -- hB0 : ¬B = 0
    change B ≠ 0 at hB0
    -- hB0 : B ≠ 0
    have hBpos : 0 < B := (Ne.le_iff_lt hB0.symm).mp hBnoneg
    intros ε hε
    -- ε : ℝ
    -- hε : ε > 0
    -- ⊢ ∃ k, ∀ (n : ℕ), n ≥ k → |(u * v) n - 0| < ε
    cases' hV (ε/B) (div_pos hε hBpos) with k hk
    -- k : ℕ
    -- hk : ∀ (n : ℕ), n ≥ k → |v n - 0| < ε / B
    use k
    -- ⊢ ∀ (n : ℕ), n ≥ k → |(u * v) n - 0| < ε
    intros n hn
    -- n : ℕ
    -- hn : n ≥ k
    -- ⊢ |(u * v) n - 0| < ε
    simp_rw [sub_zero] at *
    -- ⊢ |(u * v) n| < ε
    calc |(u * v) n|
         = |u n * v n|    := congr_arg abs (Pi.mul_apply u v n)
       _ = |u n| * |v n|  := abs_mul (u n) (v n)
       _ ≤ B * |v n|      := mul_le_mul_of_nonneg_right (hB n) (abs_nonneg _)
       _ < B * (ε/B)      := mul_lt_mul_of_pos_left (hk n hn) hBpos
       _ = ε              := mul_div_cancel' ε hB0

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

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
by
  cases' hU with B hB
  -- B : ℝ
  -- hB : ∀ (n : ℕ), |u n| ≤ B
  have hBnoneg : 0 ≤ B :=
    calc 0 ≤ |u 0| := abs_nonneg (u 0)
         _ ≤ B     := hB 0
  by_cases hB0 : B = 0
  . subst hB0
    -- hB : ∀ (n : ℕ), |u n| ≤ 0
    -- hBnoneg : 0 ≤ 0
    intros ε hε
    -- ε : ℝ
    -- hε : ε > 0
    -- ⊢ ∃ k, ∀ (n : ℕ), n ≥ k → |(u * v) n - 0| < ε
    use 0
    -- ⊢ ∀ (n : ℕ), n ≥ 0 → |(u * v) n - 0| < ε
    intros n _hn
    -- n : ℕ
    -- _hn : n ≥ 0
    -- ⊢ |(u * v) n - 0| < ε
    simp_rw [sub_zero] at *
    -- ⊢ |(u * v) n| < ε
    calc |(u * v) n|
         = |u n| * |v n| := by aesop
       _ ≤ 0 * |v n|     := mul_le_mul_of_nonneg_right (hB n) (abs_nonneg (v n))
       _ = 0             := by ring
       _ < ε             := hε
  . -- hB0 : ¬B = 0
    change B ≠ 0 at hB0
    -- hB0 : B ≠ 0
    have hBpos : 0 < B := (Ne.le_iff_lt hB0.symm).mp hBnoneg
    intros ε hε
    -- ε : ℝ
    -- hε : ε > 0
    -- ⊢ ∃ k, ∀ (n : ℕ), n ≥ k → |(u * v) n - 0| < ε
    cases' hV (ε/B) (div_pos hε hBpos) with k hk
    -- k : ℕ
    -- hk : ∀ (n : ℕ), n ≥ k → |v n - 0| < ε / B
    use k
    -- ∀ (n : ℕ), n ≥ k → |(u * v) n - 0| < ε
    intros n hn
    -- n : ℕ
    -- hn : n ≥ k
    -- ⊢ |(u * v) n - 0| < ε
    simp_rw [sub_zero] at *
    -- ⊢ |(u * v) n| < ε
    calc |(u * v) n|
         = |u n| * |v n|  := by simp [Pi.mul_apply, abs_mul]
       _ ≤ B * |v n|      := mul_le_mul_of_nonneg_right (hB n) (abs_nonneg _)
       _ < B * (ε/B)      := by aesop
       _ = ε              := mul_div_cancel' ε hB0

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

-- #variable (n : ℕ)
-- #variable (a b c : ℝ)
-- #check (abs_nonneg a : 0 ≤ |a|)
-- #check (Ne.le_iff_lt : a ≠ b → (a ≤ b ↔ a < b))
-- #check (Pi.mul_apply u v n : (u * v) n = u n * v n)
-- #check (abs_mul a b : |a * b| = |a| * |b|)
-- #check (abs_nonneg a : 0 ≤ |a|)
-- #check (div_pos : 0 < a → 0 < b → 0 < a / b)
-- #check (mul_div_cancel' a : b ≠ 0 → b * (a / b) = a)
-- #check (mul_le_mul_of_nonneg_right : a ≤ b → 0 ≤ c → a * c ≤ b * c)
-- #check (mul_lt_mul_of_pos_left : b < c → 0 < a → a * b < a * c)
-- #check (sub_zero a : a - 0 = a)
-- #check (zero_mul a : 0 * a = 0)

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

1.3. Demostraciones con Isabelle/HOL

theory Producto_de_una_sucesion_acotada_por_otra_convergente_a_cero
imports Main HOL.Real
begin

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

definition acotada :: "(nat ⇒ real) ⇒ bool"
  where "acotada u ⟷ (∃B. ∀n. ¦u n¦ ≤ B)"

lemma
  assumes "acotada u"
          "limite v 0"
  shows   "limite (λn. u n * v n) 0"
proof -
  obtain B where hB : "∀n. ¦u n¦ ≤ B"
    using assms(1) acotada_def by auto
  then have hBnoneg : "0 ≤ B" by auto
  show "limite (λn. u n * v n) 0"
  proof (cases "B = 0")
    assume "B = 0"
    show "limite (λn. u n * v n) 0"
    proof (unfold limite_def; intro allI impI)
      fix ε :: real
      assume "0 < ε"
      have "∀n≥0. ¦u n * v n - 0¦ < ε"
      proof (intro allI impI)
        fix n :: nat
        assume "n ≥ 0"
        show "¦u n * v n - 0¦ < ε"
          using ‹0 < ε› ‹B = 0› hB by auto
      qed
      then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"
        by (rule exI)
    qed
  next
    assume "B ≠ 0"
    then have hBpos : "0 < B"
      using hBnoneg by auto
    show "limite (λn. u n * v n) 0"
    proof (unfold limite_def; intro allI impI)
      fix ε :: real
      assume "0 < ε"
      then have "0 < ε/B"
        by (simp add: hBpos)
      then obtain N where hN : "∀n≥N. ¦v n - 0¦ < ε/B"
        using assms(2) limite_def by auto
      have "∀n≥N. ¦u n * v n - 0¦ < ε"
      proof (intro allI impI)
        fix n :: nat
        assume "n ≥ N"
        have "¦v n¦ < ε/B"
          using ‹N ≤ n› hN by auto
        have "¦u n * v n - 0¦ = ¦u n¦ * ¦v n¦"
          by (simp add: abs_mult)
        also have "… ≤ B * ¦v n¦"
          by (simp add: hB mult_right_mono)
        also have "… < B * (ε/B)"
          using ‹¦v n¦ < ε/B› hBpos
          by (simp only: mult_strict_left_mono)
        also have "… = ε"
          using ‹B ≠ 0› by simp
        finally show "¦u n * v n - 0¦ < ε"
          by this
      qed
      then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"
        by (rule exI)
    qed
  qed
qed

end

2. La congruencia módulo 2 es una relación de equivalencia

Se define la relación \(R\) entre los números enteros de forma que \(x\) está relacionado con \(y\) si \(x-y\) es divisible por 2.

Demostrar con Lean4 que \(R\) es una relación de equivalencia.

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

import Mathlib.Data.Int.Basic
import Mathlib.Tactic

def R (m n : ℤ) := 2 ∣ (m - n)

example : Equivalence R :=
by sorry

2.1. Demostración en lenguaje natural

Tenemos que demostrar que \(\text{ R }\) es reflexiva, simétrica y transitiva.

Para demostrar que \(\text{ R }\) es reflexiva, sea \(x ∈ ℤ\). Entonces, \(x - x = 0\) que es divisible por 2. Luego, \(x\text{ R }x\).

Para demostrar que \(\text{ R }\) es simétrica, sean \(x, y ∈ ℤ\) tales que \(x\text{ R }y\). Entonces, \(x - y\) es divisible por 2. Luego, existe un \(a ∈ ℤ\) tal que \[ x - y = 2·a \] Por tanto, \[ y - x = 2·(-a) \] Por lo que \(y - x\) es divisible por 2 y \(y\text{ R }x\).

Para demostrar que \(\text{ R }\) es transitiva, sean \(x, y, z ∈ ℤ\) tales que \(x\text{ R }y\) y \(y\text{ R }z\). Entonces, tanto \(x - y\) como \(y - z\) son divibles por 2. Luego, existen \(a, b ∈ ℤ\) tales que \begin{align} x - y &= 2·a \newline y - z &= 2·b \end{align} Por tanto, \[ x - z = 2·(a + b) \] Por lo que \(x - z\) es divisible por 2 y \(x\text{ R }z\}.

2.2. Demostraciones con Lean4

import Mathlib.Data.Int.Basic
import Mathlib.Tactic

def R (m n : ℤ) := 2 ∣ (m - n)

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

example : Equivalence R :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : ℤ), R x x
    intro x
    -- x : ℤ
    -- ⊢ R x x
    unfold R
    -- ⊢ 2 ∣ x - x
    rw [sub_self]
    -- ⊢ 2 ∣ 0
    exact dvd_zero 2
  . -- ⊢ ∀ {x y : ℤ}, R x y → R y x
    intros x y hxy
    -- x y : ℤ
    -- hxy : R x y
    -- ⊢ R y x
    unfold R at *
    -- hxy : 2 ∣ x - y
    -- ⊢ 2 ∣ y - x
    cases' hxy with a ha
    -- a : ℤ
    -- ha : x - y = 2 * a
    use -a
    -- ⊢ y - x = 2 * -a
    calc y - x
         = -(x - y) := (neg_sub x y).symm
       _ = -(2 * a) := by rw [ha]
       _ = 2 * -a   := neg_mul_eq_mul_neg 2 a
  . -- ⊢ ∀ {x y z : ℤ}, R x y → R y z → R x z
    intros x y z hxy hyz
    -- x y z : ℤ
    -- hxy : R x y
    -- hyz : R y z
    -- ⊢ R x z
    cases' hxy with a ha
    -- a : ℤ
    -- ha : x - y = 2 * a
    cases' hyz with b hb
    -- b : ℤ
    -- hb : y - z = 2 * b
    use a + b
    -- ⊢ x - z = 2 * (a + b)
    calc x - z
         = (x - y) + (y - z) := (sub_add_sub_cancel x y z).symm
       _ = 2 * a + 2 * b     := congrArg₂ (. + .) ha hb
       _ = 2 * (a + b)       := (mul_add 2 a b).symm

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

example : Equivalence R :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : ℤ), R x x
    intro x
    -- x : ℤ
    -- ⊢ R x x
    simp [R]
  . -- ⊢ ∀ {x y : ℤ}, R x y → R y x
    rintro x y ⟨a, ha⟩
    -- x y a : ℤ
    -- ha : x - y = 2 * a
    -- ⊢ R y x
    use -a
    -- ⊢ y - x = 2 * -a
    linarith
  . -- ⊢ ∀ {x y z : ℤ}, R x y → R y z → R x z
    rintro x y z ⟨a, ha⟩ ⟨b, hb⟩
    -- x y z a : ℤ
    -- ha : x - y = 2 * a
    -- b : ℤ
    -- hb : y - z = 2 * b
    -- ⊢ R x z
    use a + b
    -- ⊢ x - z = 2 * (a + b)
    linarith

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

-- variable (a b c x y x' y' : ℤ)
-- #check (congrArg₂  (. + .) : x = x' → y = y' → x + y = x' + y')
-- #check (dvd_zero a : a ∣ 0)
-- #check (mul_add a b c : a * (b + c) = a * b + a * c)
-- #check (neg_mul_eq_mul_neg a b : -(a * b) = a * -b)
-- #check (neg_sub a b : -(a - b) = b - a)
-- #check (sub_add_sub_cancel a b c : a - b + (b - c) = a - c)
-- #check (sub_self a : a - a = 0)

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

2.3. Demostraciones con Isabelle/HOL

theory La_congruencia_modulo_2_es_una_relacion_de_equivalencia
imports Main
begin

definition R :: "(int × int) set" where
  "R = {(m, n). even (m - n)}"

lemma R_iff [simp]:
  "((x, y) ∈ R) = even (x - y)"
by (simp add: R_def)

(* 1ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
  proof (unfold refl_on_def; intro conjI)
    show "R ⊆ UNIV × UNIV"
    proof -
      have "R ⊆ UNIV"
        by (rule top.extremum)
      also have "… = UNIV × UNIV"
        by (rule Product_Type.UNIV_Times_UNIV[symmetric])
      finally show "R ⊆ UNIV × UNIV"
        by this
    qed
  next
    show "∀x∈UNIV. (x, x) ∈ R"
    proof
      fix x :: int
      assume "x ∈ UNIV"
      have "even 0" by (rule even_zero)
      then have "even (x - x)" by (simp only: diff_self)
      then show "(x, x) ∈ R"
        by (simp only: R_iff)
    qed
  qed
next
  show "sym R"
  proof (unfold sym_def; intro allI impI)
    fix x y :: int
    assume "(x, y) ∈ R"
    then have "even (x - y)"
      by (simp only: R_iff)
    then show "(y, x) ∈ R"
    proof (rule evenE)
      fix a :: int
      assume ha : "x - y = 2 * a"
      have "y - x = -(x - y)"
        by (rule minus_diff_eq[symmetric])
      also have "… = -(2 * a)"
        by (simp only: ha)
      also have "… = 2 * (-a)"
        by (rule mult_minus_right[symmetric])
      finally have "y - x = 2 * (-a)"
        by this
      then have "even (y - x)"
        by (rule dvdI)
      then show "(y, x) ∈ R"
        by (simp only: R_iff)
    qed
  qed
next
  show "trans R"
  proof (unfold trans_def; intro allI impI)
    fix x y z
    assume hxy : "(x, y) ∈ R" and hyz : "(y, z) ∈ R"
    have "even (x - y)"
      using hxy by (simp only: R_iff)
    then obtain a where ha : "x - y = 2 * a"
      by (rule dvdE)
    have "even (y - z)"
      using hyz by (simp only: R_iff)
    then obtain b where hb : "y - z = 2 * b"
      by (rule dvdE)
    have "x - z = (x - y) + (y - z)"
      by simp
    also have "… = (2 * a) + (2 * b)"
      by (simp only: ha hb)
    also have "… = 2 * (a + b)"
      by (simp only: distrib_left)
    finally have "x - z = 2 * (a + b)"
      by this
    then have "even (x - z)"
      by (rule dvdI)
    then show "(x, z) ∈ R"
      by (simp only: R_iff)
  qed
qed

(* 2ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
  proof (unfold refl_on_def; intro conjI)
    show "R ⊆ UNIV × UNIV" by simp
  next
    show "∀x∈UNIV. (x, x) ∈ R"
    proof
      fix x :: int
      assume "x ∈ UNIV"
      have "x - x = 2 * 0"
        by simp
      then show "(x, x) ∈ R"
        by simp
    qed
  qed
next
  show "sym R"
  proof (unfold sym_def; intro allI impI)
    fix x y :: int
    assume "(x, y) ∈ R"
    then have "even (x - y)"
      by simp
    then obtain a where ha : "x - y = 2 * a"
      by blast
    then have "y - x = 2 *(-a)"
      by simp
    then show "(y, x) ∈ R"
      by simp
  qed
next
  show "trans R"
  proof (unfold trans_def; intro allI impI)
    fix x y z
    assume hxy : "(x, y) ∈ R" and hyz : "(y, z) ∈ R"
    have "even (x - y)"
      using hxy by simp
    then obtain a where ha : "x - y = 2 * a"
      by blast
    have "even (y - z)"
      using hyz by simp
    then obtain b where hb : "y - z = 2 * b"
      by blast
    have "x - z = 2 * (a + b)"
      using ha hb by auto
    then show "(x, z) ∈ R"
      by simp
  qed
qed

(* 3ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
  proof (unfold refl_on_def; intro conjI)
    show " R ⊆ UNIV × UNIV"
      by simp
  next
    show "∀x∈UNIV. (x, x) ∈ R"
      by simp
  qed
next
  show "sym R"
  proof (unfold sym_def; intro allI impI)
    fix x y
    assume "(x, y) ∈ R"
    then show "(y, x) ∈ R"
      by simp
  qed
next
  show "trans R"
  proof (unfold trans_def; intro allI impI)
    fix x y z
    assume "(x, y) ∈ R" and "(y, z) ∈ R"
    then show "(x, z) ∈ R"
      by simp
  qed
qed

(* 4ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
    unfolding refl_on_def by simp
next
  show "sym R"
    unfolding sym_def by simp
next
  show "trans R"
    unfolding trans_def by simp
qed

(* 5ª demostración *)

lemma "equiv UNIV R"
  unfolding equiv_def refl_on_def sym_def trans_def
  by simp

(* 6ª demostración *)

lemma "equiv UNIV R"
  by (simp add: equiv_def refl_on_def sym_def trans_def)

end

3. Las funciones con inversa por la izquierda son inyectivas

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

y que \(f\) tenga inversa por la izquierda está definido por

   HasLeftInverse (f : α → β) : Prop :=
      ∃ finv : β → α, LeftInverse finv f

Finalmente, que \(f\) es inyectiva está definido por

   Injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

Demostrar con Lean4 que si \(f\) tiene inversa por la izquierda, entonces \(f\) es inyectiva.

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

import Mathlib.Tactic
open Function

universe u v
variable {α : Type u}
variable {β : Type v}
variable {f : α → β}

example
  (hf : HasLeftInverse f)
  : Injective f :=
by sorry

3.1. Demostración en lenguaje natural

Sea \(f: A → B\) que tiene inversa por la izquierda. Entonces, existe una \(g: B → A) tal que \[ (∀ x ∈ A)[g(f(x)) = x] \tag{1} \] Para demostrar que \(f\) es inyectiva, sean \(x, y ∈ A\) tales que \[ f(x) = f(y) \] Entonces, \[ g(f(x)) = g(f(y)) \] y, por (1), \[ x = y \]

3.2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

universe u v
variable {α : Type u}
variable {β : Type v}
variable {f : α → β}

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

example
  (hf : HasLeftInverse f)
  : Injective f :=
by
  intros x y hxy
  -- x y : α
  -- hxy : f x = f y
  -- ⊢ x = y
  unfold HasLeftInverse at hf
  -- hf : ∃ finv, LeftInverse finv f
  unfold LeftInverse at hf
  -- hf : ∃ finv, ∀ (x : α), finv (f x) = x
  cases' hf with g hg
  -- g : β → α
  -- hg :
  calc x = g (f x) := (hg x).symm
       _ = g (f y) := congr_arg g hxy
       _ = y       := hg y

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

example
  (hf : HasLeftInverse f)
  : Injective f :=
by
  intros x y hxy
  -- x y : α
  -- hxy : f x = f y
  -- ⊢ x = y
  cases' hf with g hg
  -- g : β → α
  -- hg : LeftInverse g f
  calc x = g (f x) := (hg x).symm
       _ = g (f y) := congr_arg g hxy
       _ = y       := hg y

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

example
  (hf : HasLeftInverse f)
  : Injective f :=
by
  apply Exists.elim hf
  -- ⊢ ∀ (a : β → α), LeftInverse a f → Injective f
  intro g hg
  -- g : β → α
  -- hg : LeftInverse g f
  -- ⊢ Injective f
  exact LeftInverse.injective hg

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

example
  (hf : HasLeftInverse f)
  : Injective f :=
Exists.elim hf (fun _g hg ↦ LeftInverse.injective hg)

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

example
  (hf : HasLeftInverse f)
  : Injective f :=
HasLeftInverse.injective hf

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

-- variable (x y : α)
-- variable (p : α → Prop)
-- variable (b : Prop)
-- variable (g : β → α)
-- #check (Exists.elim : (∃ x, p x) → (∀ x, p x → b) → b)
-- #check (LeftInverse.injective : LeftInverse g f → Injective f)
-- #check (congr_arg f : x = y → f x = f y)

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

3.3. Demostraciones con Isabelle/HOL

theory Las_funciones_con_inversa_por_la_izquierda_son_inyectivas
imports Main
begin

definition tiene_inversa_izq :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa_izq f ⟷ (∃g. ∀x. g (f x) = x)"

(* 1ª demostración *)

lemma
  assumes "tiene_inversa_izq f"
  shows   "inj f"
proof (unfold inj_def; intro allI impI)
  fix x y
  assume "f x = f y"
  obtain g where hg : "∀x. g (f x) = x"
    using assms tiene_inversa_izq_def by auto
  have "x = g (f x)"
    by (simp only: hg)
  also have "… = g (f y)"
    by (simp only: ‹f x = f y›)
  also have "… = y"
    by (simp only: hg)
  finally show "x = y" .
qed

(* 2ª demostración *)

lemma
  assumes "tiene_inversa_izq f"
  shows   "inj f"
  by (metis assms inj_def tiene_inversa_izq_def)

end

4. Si el límite de la sucesión uₙ es a, entonces el límite de -uₙ es -a

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

Se define que (c) es el límite de la sucesión (u), por

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

Demostrar con Lean4 que que si el límite de (uₙ) es (a), entonces el de (-uₙ) es (-a).

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

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

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

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

example
  (h : limite u a)
  : limite (fun n ↦ -u n) (-a) :=
by sorry

4.1. Demostración en lenguaje natural

Sea (ε ∈ ℝ) tal que (ε > 0). Tenemos que demostrar que [ (∃ N ∈ ℕ)(∀ n ≥ N)[|-uₙ - -a| < ε] \tag{1} ] Puesto que el límite de (uₙ) es (a), existe un (k ∈ ℕ) tal que [ (∀ n ≥ k)[|uₙ - a| < ε/|c| \tag{2} ] Veamos que con (k) se cumple (1). En efecto, sea (n ≥ k). Entonces, \begin{align} |-uₙ - -a| &= |-(uₙ - a)| \ &= |uₙ - a| \ &< ε &&\text{[por (2)]} \end{align}

4.2. Demostraciones con Lean4

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

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

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

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

example
  (h : limite u a)
  : limite (fun n ↦ -u n) (-a) :=
by
  unfold limite at *
  -- h : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε
  -- ⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => -u n) n - -a| < ε
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |(fun n => -u n) n - -a| < ε
  specialize h ε hε
  -- h : ∃ N, ∀ (n : ℕ), n ≥ N → |u n - a| < ε
  cases' h with k hk
  -- k : ℕ
  -- hk : ∀ (n : ℕ), n ≥ k → |u n - a| < ε
  use k
  -- ⊢ ∀ (n : ℕ), n ≥ k → |(fun n => -u n) n - -a| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |(fun n => -u n) n - -a| < ε
  calc |(fun n => -u n) n - -a|
       = |(-u n - -a)|          := rfl
     _ = |(-(u n - a))|         := by congr ; ring
     _ = |(u n - a)|            := abs_neg (u n - a)
     _ < ε                      := hk n hn

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

-- #check (abs_neg a : |(-a)| = |a|)

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

4.3. Demostraciones con Isabelle/HOL

theory Limite_de_la_opuesta
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"
  shows   "limite (λ n. -u n) (-a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦-u n - -a¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"
      using assms limite_def
      by auto
    have "∀n≥N. ¦-u n - -a¦ < ε"
      proof (intro allI impI)
        fix n
        assume "n ≥ N"
        have "¦-u n - -a¦ = ¦u n - a¦"
          by argo
        also have "… < ε"
          using hN ‹n ≥ N›
          by simp
        finally show "¦-u n - -a¦ < ε"
          by simp
    qed
    then show "∃k. ∀n≥k. ¦-u n - -a¦ < ε"
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦-u n - -a¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"
      using assms limite_def
      by auto
    have "∀n≥N. ¦-u n - -a¦ < ε"
      using hN by fastforce
    then show "∃k. ∀n≥k. ¦-u n - -a¦ < ε"
      by (rule exI)
  qed
qed

(* 3ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦-u n - -a¦ < ε"
    using assms limite_def by force
qed

(* 4ª demostración *)

lemma
  assumes "limite u a"
  shows   "limite (λ n. -u n) (-a)"
using assms limite_def by force

end

5. Si g ∘ f es inyectiva, entonces f es inyectiva

Sean \(f: X → Y\) y \(g: Y → Z\). Demostrar con Lean4 que si \(g ∘ f\) es inyectiva, entonces \(f\) es inyectiva.

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

import Mathlib.Tactic

open Function

variable {X Y Z : Type}
variable {f : X → Y}
variable {g : Y → Z}

example
  (h : Injective (g ∘ f))
  : Injective f :=
by sorry

5.1. Demostración en lenguaje natural

Sean \(a, b ∈ X\) tales que \[ f(a) = f(b) \] Entonces, \[ g(f(a)) = g(f(b)) \] Luego \[ (g ∘ f)(a) = (g ∘ f)(b) \] y, como g ∘ f es inyectiva, \[ a = b \]

5.2. Demostraciones con Lean4

import Mathlib.Tactic

open Function

variable {X Y Z : Type}
variable {f : X → Y}
variable {g : Y → Z}

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

example
  (h : Injective (g ∘ f))
  : Injective f :=
by
  intro a b hab
  -- a b : X
  -- hab : f a = f b
  -- ⊢ a = b
  have h1 : (g ∘ f) a = (g ∘ f) b := by simp_all only [comp_apply]
  exact h h1

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

example
  (h : Injective (g ∘ f))
  : Injective f :=
by
  intro a b hab
  -- a b : X
  -- hab : f a = f b
  -- ⊢ a = b
  apply h
  -- ⊢ (g ∘ f) a = (g ∘ f) b
  change g (f a) = g (f b)
  -- ⊢ g (f a) = g (f b)
  rw [hab]

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

-- variable (x : X)
-- #check (Function.comp_apply : (g ∘ f) x = g (f x))

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

5.3. Demostraciones con Isabelle/HOL

theory Inyectiva_si_lo_es_la_composicion
imports Main
begin

(* 1ª demostración *)

lemma
  assumes "inj (g ∘ f)"
  shows "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  show "x = y"
  proof -
    have "g (f x) = g (f y)"
      using ‹f x = f y›
      by simp
    then have "(g ∘ f) x = (g ∘ f) y"
      by simp
    with assms show "x = y"
      by (rule injD)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "inj (g ∘ f)"
  shows "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  then show "x = y"
    using assms injD by fastforce
qed

(* 3ª demostración *)

lemma
  assumes "inj (g ∘ f)"
  shows "inj f"
using assms
by (rule inj_on_imageI2)

(* Nota: Al calcular el cursor en shows sale una sugerencia indicando
   que se puede demostrar con la regla inj_on_imageI2. *)

end