La semana en Calculemus (4 de mayo de 2024)

José A. Alonso

04-05-2024

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

1. Imagen de la interseccion general mediante aplicaciones inyectivas
2. Imagen inversa de la unión general
3. Imagen inversa de la intersección general
4. Teorema de Cantor
5. En los monoides, los inversos a la izquierda y a la derecha son iguales

A continuación se muestran las soluciones.

1. Imagen de la interseccion general mediante aplicaciones inyectivas

Demostrar con Lean4 que si \(f\) es inyectiva, entonces \[⋂ᵢf[Aᵢ] ⊆ f\left[⋂ᵢAᵢ\right] \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set Function

variable {α β I : Type _}
variable (f : α → β)
variable (A : I → Set α)

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
sorry

1.1. Demostración en lenguaje natural

Sea \(y ∈ ⋂ᵢf[Aᵢ]\). Entonces, \begin{align} & (∀i ∈ I)y ∈ f[Aᵢ] \tag{1} \newline & y ∈ f[Aᵢ] \end{align} Por tanto, existe un \(x ∈ Aᵢ\) tal que \[ f(x) = y \tag{2} \]

Veamos que \(x ∈ ⋂ᵢAᵢ\). Para ello, sea \(j ∈ I\). Por (1), \[ y ∈ f[Aⱼ] \] Luego, existe un \(z\) tal que \begin{align} &z ∈ Aⱼ \tag{3} \newline &f(z) = y \end{align} Pot (2), \[ f(x) = f(z) \] y, por ser \(f\) inyectiva, \[ x = z \] y, por (3), \[ x ∈ Aⱼ \]

Puesto que \(x ∈ ⋂ᵢAᵢ\) se tiene que \(f(x) ∈ f\left[⋂ᵢAᵢ\right]\) y, por (2), \(y ∈ f\left[⋂ᵢAᵢ\right]\).

1.2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set Function

variable {α β I : Type _}
variable (f : α → β)
variable (A : I → Set α)

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

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
  intros y hy
  -- y : β
  -- hy : y ∈ ⋂ (i : I), f '' A i
  -- ⊢ y ∈ f '' ⋂ (i : I), A i
  have h1 : ∀ (i : I), y ∈ f '' A i := mem_iInter.mp hy
  have h2 : y ∈ f '' A i := h1 i
  obtain ⟨x : α, h3 : x ∈ A i ∧ f x = y⟩ := h2
  have h4 : f x = y := h3.2
  have h5 : ∀ i : I, x ∈ A i := by
    intro j
    have h5a : y ∈ f '' A j := h1 j
    obtain ⟨z : α, h5b : z ∈ A j ∧ f z = y⟩ := h5a
    have h5c : z ∈ A j := h5b.1
    have h5d : f z = y := h5b.2
    have h5e : f z = f x := by rwa [←h4] at h5d
    have h5f : z = x := injf h5e
    show x ∈ A j
    rwa [h5f] at h5c
  have h6 : x ∈ ⋂ i, A i := mem_iInter.mpr h5
  have h7 : f x ∈ f '' (⋂ i, A i) := mem_image_of_mem f h6
  show y ∈ f '' (⋂ i, A i)
  rwa [h4] at h7

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

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
  intros y hy
  -- y : β
  -- hy : y ∈ ⋂ (i : I), f '' A i
  -- ⊢ y ∈ f '' ⋂ (i : I), A i
  rw [mem_iInter] at hy
  -- hy : ∀ (i : I), y ∈ f '' A i
  rcases hy i with ⟨x, -, fxy⟩
  -- x : α
  -- fxy : f x = y
  use x
  -- ⊢ x ∈ ⋂ (i : I), A i ∧ f x = y
  constructor
  . -- ⊢ x ∈ ⋂ (i : I), A i
    apply mem_iInter_of_mem
    -- ⊢ ∀ (i : I), x ∈ A i
    intro j
    -- j : I
    -- ⊢ x ∈ A j
    rcases hy j with ⟨z, zAj, fzy⟩
    -- z : α
    -- zAj : z ∈ A j
    -- fzy : f z = y
    convert zAj
    -- ⊢ x = z
    apply injf
    -- ⊢ f x = f z
    rw [fxy]
    -- ⊢ y = f z
    rw [←fzy]
  . -- ⊢ f x = y
    exact fxy

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

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
  intro y
  -- y : β
  -- ⊢ y ∈ ⋂ (i : I), f '' A i → y ∈ f '' ⋂ (i : I), A i
  simp
  -- ⊢ (∀ (i : I), ∃ x, x ∈ A i ∧ f x = y) → ∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y
  intro h
  -- h : ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y
  -- ⊢ ∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y
  rcases h i with ⟨x, -, fxy⟩
  -- x : α
  -- fxy : f x = y
  use x
  -- ⊢ (∀ (i : I), x ∈ A i) ∧ f x = y
  constructor
  . -- ⊢ ∀ (i : I), x ∈ A i
    intro j
    -- j : I
    -- ⊢ x ∈ A j
    rcases h j with ⟨z, zAi, fzy⟩
    -- z : α
    -- zAi : z ∈ A j
    -- fzy : f z = y
    have : f x = f z := by rw [fxy, fzy]
    -- this : f x = f z
    have : x = z := injf this
    -- this : x = z
    rw [this]
    -- ⊢ z ∈ A j
    exact zAi
  . -- ⊢ f x = y
    exact fxy

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

-- variable (x : α)
-- variable (s : Set α)
-- #check (mem_iInter : x ∈ ⋂ i, A i ↔ ∀ i, x ∈ A i)
-- #check (mem_iInter_of_mem : (∀ i, x ∈ A i) → x ∈ ⋂ i, A i)
-- #check (mem_image_of_mem f : x  ∈ s → f x ∈ f '' s)

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

1.3. Demostraciones con Isabelle/HOL

theory Imagen_de_la_interseccion_general_mediante_inyectiva
imports Main
begin

(* 1ª demostración *)

lemma
  assumes "i ∈ I"
          "inj f"
  shows "(⋂ i ∈ I. f ` A i) ⊆ f ` (⋂ i ∈ I. A i)"
proof (rule subsetI)
  fix y
  assume "y ∈ (⋂ i ∈ I. f ` A i)"
  then have "y ∈ f ` A i"
    using ‹i ∈ I› by (rule INT_D)
  then show "y ∈ f ` (⋂ i ∈ I. A i)"
  proof (rule imageE)
    fix x
    assume "y = f x"
    assume "x ∈ A i"
    have "x ∈ (⋂ i ∈ I. A i)"
    proof (rule INT_I)
      fix j
      assume "j ∈ I"
      show "x ∈ A j"
      proof -
        have "y ∈ f ` A j"
          using ‹y ∈ (⋂i∈I. f ` A i)› ‹j ∈ I› by (rule INT_D)
        then show "x ∈ A j"
        proof (rule imageE)
          fix z
          assume "y = f z"
          assume "z ∈ A j"
          have "f z = f x"
            using ‹y = f z› ‹y = f x› by (rule subst)
          with ‹inj f› have "z = x"
            by (rule injD)
          then show "x ∈ A j"
            using ‹z ∈ A j› by (rule subst)
        qed
      qed
    qed
    then have "f x ∈ f ` (⋂ i ∈ I. A i)"
      by (rule imageI)
    with ‹y = f x› show "y ∈ f ` (⋂ i ∈ I. A i)"
      by (rule ssubst)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "i ∈ I"
          "inj f"
  shows "(⋂ i ∈ I. f ` A i) ⊆ f ` (⋂ i ∈ I. A i)"
proof
  fix y
  assume "y ∈ (⋂ i ∈ I. f ` A i)"
  then have "y ∈ f ` A i" using ‹i ∈ I› by simp
  then show "y ∈ f ` (⋂ i ∈ I. A i)"
  proof
    fix x
    assume "y = f x"
    assume "x ∈ A i"
    have "x ∈ (⋂ i ∈ I. A i)"
    proof
      fix j
      assume "j ∈ I"
      show "x ∈ A j"
      proof -
        have "y ∈ f ` A j"
          using ‹y ∈ (⋂i∈I. f ` A i)› ‹j ∈ I› by simp
        then show "x ∈ A j"
        proof
          fix z
          assume "y = f z"
          assume "z ∈ A j"
          have "f z = f x" using ‹y = f z› ‹y = f x› by simp
          with ‹inj f› have "z = x" by (rule injD)
          then show "x ∈ A j" using ‹z ∈ A j› by simp
        qed
      qed
    qed
    then have "f x ∈ f ` (⋂ i ∈ I. A i)" by simp
    with ‹y = f x› show "y ∈ f ` (⋂ i ∈ I. A i)" by simp
  qed
qed

(* 3ª demostración *)

lemma
  assumes "i ∈ I"
          "inj f"
  shows "(⋂ i ∈ I. f ` A i) ⊆ f ` (⋂ i ∈ I. A i)"
  using assms
  by (simp add: image_INT)

end

2. Imagen inversa de la unión general

Demostrar con Lean4 que \[ f⁻¹\left[⋃ᵢ Bᵢ\right] = ⋃ᵢ f⁻¹[Bᵢ] \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by sorry

2.1. Demostración en lenguaje natural

Tenemos que demostrar que, para todo \(x\), \[ x ∈ f⁻¹\left[⋃ᵢ Bᵢ\right] ↔ x ∈ ⋃ᵢ f⁻¹[Bᵢ] \] y lo haremos demostrando las dos implicaciones.

(⟹) Supongamos que \(x ∈ f⁻¹\left[⋃ᵢ Bᵢ\right]\). Entonces, por la definición de la imagen inversa, \[ f(x) ∈ ⋃ᵢ Bᵢ \] y, por la definición de la unión, existe un \(i\) tal que \[ f(x) ∈ Bᵢ \] y, por la definición de la imagen inversa, \[ x ∈ f⁻¹[Bᵢ] \] y, por la definición de la unión, \[ x ∈ ⋃ᵢ f⁻¹[Bᵢ] \]

(⟸) Supongamos que \(x ∈ ⋃ᵢ f⁻¹[Bᵢ]\). Entonces, por la definición de la unión, existe un \(i\) tal que \[ x ∈ f⁻¹[Bᵢ] \] y, por la definición de la imagen inversa, \[ f(x) ∈ Bᵢ \] y, por la definición de la unión, \[ f(x) ∈ ⋃ᵢ Bᵢ \] y, por la definición de la imagen inversa, \[ x ∈ f⁻¹\left[⋃ᵢ Bᵢ\right] \]

2.2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ f ⁻¹' ⋃ (i : I), B i ↔ x ∈ ⋃ (i : I), f ⁻¹' B i
  constructor
  . -- ⊢ x ∈ f ⁻¹' ⋃ (i : I), B i → x ∈ ⋃ (i : I), f ⁻¹' B i
    intro hx
    -- hx : x ∈ f ⁻¹' ⋃ (i : I), B i
    -- ⊢ x ∈ ⋃ (i : I), f ⁻¹' B i
    rw [mem_preimage] at hx
    -- hx : f x ∈ ⋃ (i : I), B i
    rw [mem_iUnion] at hx
    -- hx : ∃ i, f x ∈ B i
    cases' hx with i fxBi
    -- i : I
    -- fxBi : f x ∈ B i
    rw [mem_iUnion]
    -- ⊢ ∃ i, x ∈ f ⁻¹' B i
    use i
    -- ⊢ x ∈ f ⁻¹' B i
    apply mem_preimage.mpr
    -- ⊢ f x ∈ B i
    exact fxBi
  . -- ⊢ x ∈ ⋃ (i : I), f ⁻¹' B i → x ∈ f ⁻¹' ⋃ (i : I), B i
    intro hx
    -- hx : x ∈ ⋃ (i : I), f ⁻¹' B i
    -- ⊢ x ∈ f ⁻¹' ⋃ (i : I), B i
    rw [mem_preimage]
    -- ⊢ f x ∈ ⋃ (i : I), B i
    rw [mem_iUnion]
    -- ⊢ ∃ i, f x ∈ B i
    rw [mem_iUnion] at hx
    -- hx : ∃ i, x ∈ f ⁻¹' B i
    cases' hx with i xBi
    -- i : I
    -- xBi : x ∈ f ⁻¹' B i
    use i
    -- ⊢ f x ∈ B i
    rw [mem_preimage] at xBi
    -- xBi : f x ∈ B i
    exact xBi

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
preimage_iUnion

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

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by  simp

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

-- variable (x : α)
-- variable (s : Set β)
-- variable (A : I → Set α)
-- #check (mem_iUnion : x ∈ ⋃ i, A i ↔ ∃ i, x ∈ A i)
-- #check (mem_preimage : x ∈ f ⁻¹' s ↔ f x ∈ s)
-- #check (preimage_iUnion : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i))

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

2.3. Demostraciones con Isabelle/HOL

theory Imagen_inversa_de_la_union_general
imports Main
begin

(* 1ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
proof (rule equalityI)
  show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (⋃ i ∈ I. B i)"
    then have "f x ∈ (⋃ i ∈ I. B i)"
      by (rule vimageD)
    then show "x ∈ (⋃ i ∈ I. f -` B i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "f x ∈ B i"
      then have "x ∈ f -` B i"
        by (rule vimageI2)
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)"
        by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋃ i ∈ I. f -` B i)"
    then show "x ∈ f -` (⋃ i ∈ I. B i)"
    proof (rule UN_E)
      fix i
      assume "i ∈ I"
      assume "x ∈ f -` B i"
      then have "f x ∈ B i"
        by (rule vimageD)
      with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)"
        by (rule UN_I)
      then show "x ∈ f -` (⋃ i ∈ I. B i)"
        by (rule vimageI2)
    qed
  qed
qed

(* 2ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
proof
  show "f -` (⋃ i ∈ I. B i) ⊆ (⋃ i ∈ I. f -` B i)"
  proof
    fix x
    assume "x ∈ f -` (⋃ i ∈ I. B i)"
    then have "f x ∈ (⋃ i ∈ I. B i)" by simp
    then show "x ∈ (⋃ i ∈ I. f -` B i)"
    proof
      fix i
      assume "i ∈ I"
      assume "f x ∈ B i"
      then have "x ∈ f -` B i" by simp
      with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. f -` B i)" by (rule UN_I)
    qed
  qed
next
  show "(⋃ i ∈ I. f -` B i) ⊆ f -` (⋃ i ∈ I. B i)"
  proof
    fix x
    assume "x ∈ (⋃ i ∈ I. f -` B i)"
    then show "x ∈ f -` (⋃ i ∈ I. B i)"
    proof
      fix i
      assume "i ∈ I"
      assume "x ∈ f -` B i"
      then have "f x ∈ B i" by simp
      with ‹i ∈ I› have "f x ∈ (⋃ i ∈ I. B i)" by (rule UN_I)
      then show "x ∈ f -` (⋃ i ∈ I. B i)" by simp
    qed
  qed
qed

(* 3ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
  by (simp only: vimage_UN)

(* 4ª demostración *)

lemma "f -` (⋃ i ∈ I. B i) = (⋃ i ∈ I. f -` B i)"
  by auto

end

3. Imagen inversa de la intersección general

Demostrar con Lean4 que \[ f⁻¹\left[\bigcap_{i \in I} B_i\right] = \bigcap_{i \in I} f⁻¹[B_i] \]

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

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by sorry

3.1. Demostración en lenguaje natural

Se demuestra mediante la siguiente cadena de equivalencias \begin{align} x ∈ f⁻¹\left[\bigcap_{i \in I} B_i\right] &↔ f(x) ∈ \bigcap_{i \in I} B_i \newline &↔ (∀ i) f(x) ∈ B_i \newline &↔ (∀ i) x ∈ f⁻¹[B_i] \newline &↔ x ∈ \bigcap_{i \in I} f⁻¹[B_i] \end{align}

3.2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i ↔ x ∈ ⋂ (i : I), f ⁻¹' B i
  calc  (x ∈ f ⁻¹' ⋂ i, B i)
     ↔ f x ∈ ⋂ i, B i       := mem_preimage
   _ ↔ (∀ i, f x ∈ B i)     := mem_iInter
   _ ↔ (∀ i, x ∈ f ⁻¹' B i) := iff_of_eq rfl
   _ ↔ x ∈ ⋂ i, f ⁻¹' B i   := mem_iInter.symm

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by
  ext x
  -- x : α
  -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i ↔ x ∈ ⋂ (i : I), f ⁻¹' B i
  constructor
  . -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i → x ∈ ⋂ (i : I), f ⁻¹' B i
    intro hx
    -- hx : x ∈ f ⁻¹' ⋂ (i : I), B i
    -- ⊢ x ∈ ⋂ (i : I), f ⁻¹' B i
    apply mem_iInter_of_mem
    -- ⊢ ∀ (i : I), x ∈ f ⁻¹' B i
    intro i
    -- i : I
    -- ⊢ x ∈ f ⁻¹' B i
    rw [mem_preimage]
    -- ⊢ f x ∈ B i
    rw [mem_preimage] at hx
    -- hx : f x ∈ ⋂ (i : I), B i
    rw [mem_iInter] at hx
    -- hx : ∀ (i : I), f x ∈ B i
    exact hx i
  . -- ⊢ x ∈ ⋂ (i : I), f ⁻¹' B i → x ∈ f ⁻¹' ⋂ (i : I), B i
    intro hx
    -- hx : x ∈ ⋂ (i : I), f ⁻¹' B i
    -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i
    rw [mem_preimage]
    -- ⊢ f x ∈ ⋂ (i : I), B i
    rw [mem_iInter]
    -- ⊢ ∀ (i : I), f x ∈ B i
    intro i
    -- i : I
    -- ⊢ f x ∈ B i
    rw [←mem_preimage]
    -- ⊢ x ∈ f ⁻¹' B i
    rw [mem_iInter] at hx
    -- hx : ∀ (i : I), x ∈ f ⁻¹' B i
    exact hx i

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by
  ext x
  -- ⊢ x ∈ f ⁻¹' ⋂ (i : I), B i ↔ x ∈ ⋂ (i : I), f ⁻¹' B i
  simp

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

example : f ⁻¹' (⋂ i, B i) = ⋂ i, f ⁻¹' (B i) :=
by { ext ; simp }

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

-- variable (x : α)
-- variable (s : Set β)
-- variable (A : I → Set α)
-- variable (a b : Prop)
-- #check (iff_of_eq : a = b → (a ↔ b))
-- #check (mem_iInter : x ∈ ⋂ i, A i ↔ ∀ i, x ∈ A i)
-- #check (mem_iInter_of_mem : (∀ i, x ∈ A i) → x ∈ ⋂ i, A i)
-- #check (mem_preimage : x ∈ f ⁻¹' s ↔ f x ∈ s)

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

3.3. Demostraciones con Isabelle/HOL

theory Imagen_inversa_de_la_interseccion_general
imports Main
begin

(* 1ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
proof (rule equalityI)
  show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ f -` (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. f -` B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      have "f x ∈ (⋂ i ∈ I. B i)"
        using ‹x ∈ f -` (⋂ i ∈ I. B i)› by (rule vimageD)
      then have "f x ∈ B i"
        using ‹i ∈ I› by (rule INT_D)
      then show "x ∈ f -` B i"
        by (rule vimageI2)
    qed
  qed
next
  show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"
  proof (rule subsetI)
    fix x
    assume "x ∈ (⋂ i ∈ I. f -` B i)"
    have "f x ∈ (⋂ i ∈ I. B i)"
    proof (rule INT_I)
      fix i
      assume "i ∈ I"
      with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i"
        by (rule INT_D)
      then show "f x ∈ B i"
        by (rule vimageD)
    qed
    then show "x ∈ f -` (⋂ i ∈ I. B i)"
      by (rule vimageI2)
  qed
qed

(* 2ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
proof
  show "f -` (⋂ i ∈ I. B i) ⊆ (⋂ i ∈ I. f -` B i)"
  proof (rule subsetI)
    fix x
    assume hx : "x ∈ f -` (⋂ i ∈ I. B i)"
    show "x ∈ (⋂ i ∈ I. f -` B i)"
    proof
      fix i
      assume "i ∈ I"
      have "f x ∈ (⋂ i ∈ I. B i)" using hx by simp
      then have "f x ∈ B i" using ‹i ∈ I› by simp
      then show "x ∈ f -` B i" by simp
    qed
  qed
next
  show "(⋂ i ∈ I. f -` B i) ⊆ f -` (⋂ i ∈ I. B i)"
  proof
    fix x
    assume "x ∈ (⋂ i ∈ I. f -` B i)"
    have "f x ∈ (⋂ i ∈ I. B i)"
    proof
      fix i
      assume "i ∈ I"
      with ‹x ∈ (⋂ i ∈ I. f -` B i)› have "x ∈ f -` B i" by simp
      then show "f x ∈ B i" by simp
    qed
    then show "x ∈ f -` (⋂ i ∈ I. B i)" by simp
  qed
qed

(* 3 demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
  by (simp only: vimage_INT)

(* 4ª demostración *)

lemma "f -` (⋂ i ∈ I. B i) = (⋂ i ∈ I. f -` B i)"
  by auto

end

4. Teorema de Cantor

Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en el conjunto de sus subconjuntos.

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

import Mathlib.Data.Set.Basic
open Function

variable {α : Type}

example : ∀ f : α → Set α, ¬Surjective f :=
by sorry

4.1. Demostración en lenguaje natural

Sea \(f\) una función de \(A\) en el conjunto de los subconjuntos \(A\). Tenemos que demostrar que \(f\) no es suprayectiva. Lo haremos por reducción al absurdo. Para ello, supongamos que \(f\) es suprayectiva y consideremos el conjunto \[ S := \{i ∈ A | i ∉ f(i)\} \tag{1} \] Entonces, tiene que existir un \(j ∈ A\) tal que \[ f(j) = S \tag{2} \] Se pueden dar dos casos: \(j ∈ S\) ó \(j ∉ S\). Veamos que ambos son imposibles.

Caso 1: Supongamos que \(j ∈ S\). Entonces, por (1) \[ j ∉ f(j) \] y, por (2), \[ j ∉ S \] que es una contradicción.

Caso 2: Supongamos que \(j ∉ S\). Entonces, por (1) \[ j ∈ f(j) \] y, por (2), \[ j ∈ S \] que es una contradicción.

4.2. Demostraciones con Lean4

import Mathlib.Data.Set.Basic
open Function

variable {α : Type}

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

example : ∀ f : α → Set α, ¬Surjective f :=
by
  intros f hf
  -- f : α → Set α
  -- hf : Surjective f
  -- ⊢ False
  let S := {i | i ∉ f i}
  unfold Surjective at hf
  -- hf : ∀ (b : Set α), ∃ a, f a = b
  cases' hf S with j hj
  -- j : α
  -- hj : f j = S
  by_cases j ∈ S
  . -- h : j ∈ S
    dsimp at h
    -- h : ¬j ∈ f j
    apply h
    -- ⊢ j ∈ f j
    rw [hj]
    -- ⊢ j ∈ S
    exact h
  . -- h : ¬j ∈ S
    apply h
    -- ⊢ j ∈ S
    rw [←hj] at h
    -- h : ¬j ∈ f j
    exact h

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

example : ∀ f : α → Set α, ¬ Surjective f :=
by
  intros f hf
  -- f : α → Set α
  -- hf : Surjective f
  -- ⊢ False
  let S := {i | i ∉ f i}
  cases' hf S with j hj
  -- j : α
  -- hj : f j = S
  by_cases j ∈ S
  . -- h : j ∈ S
    apply h
    -- ⊢ j ∈ f j
    rwa [hj]
  . -- h : ¬j ∈ S
    apply h
    rwa [←hj] at h

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

example : ∀ f : α → Set α, ¬ Surjective f :=
by
  intros f hf
  -- f : α → Set α
  -- hf : Surjective f
  -- ⊢ False
  let S := {i | i ∉ f i}
  cases' hf S with j hj
  -- j : α
  -- hj : f j = S
  have h : (j ∈ S) = (j ∉ S) :=
    calc  (j ∈ S)
       = (j ∉ f j) := Set.mem_setOf_eq
     _ = (j ∉ S)   := congrArg (j ∉ .) hj
  exact iff_not_self (iff_of_eq h)

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

example : ∀ f : α → Set α, ¬ Surjective f :=
cantor_surjective

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

-- variable (x : α)
-- variable (p : α → Prop)
-- variable (a b : Prop)
-- #check (Set.mem_setOf_eq : (x ∈ {y : α | p y}) = p x)
-- #check (iff_of_eq : a = b → (a ↔ b))
-- #check (iff_not_self : ¬(a ↔ ¬a))
-- #check (cantor_surjective : ∀ f : α → Set α, ¬ Surjective f)

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

4.3. Demostraciones con Isabelle/HOL

theory Teorema_de_Cantor
imports Main
begin

(* 1ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof (rule notI)
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j"
    using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j"
    by (rule exE)
  show False
  proof (cases "j ∈ ?S")
    assume "j ∈ ?S"
    then have "j ∉ f j"
      by (rule CollectD)
    moreover
    have "j ∈ f j"
      using ‹?S = f j› ‹j ∈ ?S› by (rule subst)
    ultimately show False
      by (rule notE)
  next
    assume "j ∉ ?S"
    with ‹?S = f j› have "j ∉ f j"
      by (rule subst)
    then have "j ∈ ?S"
      by (rule CollectI)
    with ‹j ∉ ?S› show False
      by (rule notE)
  qed
qed

(* 2ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof (rule notI)
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j"
    using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j"
    by (rule exE)
  have "j ∉ ?S"
  proof (rule notI)
    assume "j ∈ ?S"
    then have "j ∉ f j"
      by (rule CollectD)
    with ‹?S = f j› have "j ∉ ?S"
      by (rule ssubst)
    then show False
      using ‹j ∈ ?S› by (rule notE)
  qed
  moreover
  have "j ∈ ?S"
  proof (rule CollectI)
    show "j ∉ f j"
    proof (rule notI)
      assume "j ∈ f j"
      with ‹?S = f j› have "j ∈ ?S"
        by (rule ssubst)
      then have "j ∉ f j"
        by (rule CollectD)
      then show False
        using ‹j ∈ f j› by (rule notE)
    qed
  qed
  ultimately show False
    by (rule notE)
qed

(* 3ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j" by (rule exE)
  have "j ∉ ?S"
  proof
    assume "j ∈ ?S"
    then have "j ∉ f j" by simp
    with ‹?S = f j› have "j ∉ ?S" by simp
    then show False using ‹j ∈ ?S› by simp
  qed
  moreover
  have "j ∈ ?S"
  proof
    show "j ∉ f j"
    proof
      assume "j ∈ f j"
      with ‹?S = f j› have "j ∈ ?S" by simp
      then have "j ∉ f j" by simp
      then show False using ‹j ∈ f j› by simp
    qed
  qed
  ultimately show False by simp
qed

(* 4ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof (rule notI)
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j"
    using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j"
    by (rule exE)
  have "j ∈ ?S = (j ∉ f j)"
    by (rule mem_Collect_eq)
  also have "… = (j ∉ ?S)"
    by (simp only: ‹?S = f j›)
  finally show False
    by (simp only: simp_thms(10))
qed

(* 5ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
proof
  assume "surj f"
  let ?S = "{i. i ∉ f i}"
  have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD)
  then obtain j where "?S = f j" by (rule exE)
  have "j ∈ ?S = (j ∉ f j)" by simp
  also have "… = (j ∉ ?S)" using ‹?S = f j› by simp
  finally show False by simp
qed

(* 6ª demostración *)

theorem
  fixes f :: "'α ⇒ 'α set"
  shows "¬ surj f"
  unfolding surj_def
  by best

end

5. En los monoides, los inversos a la izquierda y a la derecha son iguales

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

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 que si \(M\) es un monoide, \(a ∈ M\), \(b\) es un inverso de \(a\) por la izquierda y \(c\) es un inverso de \(a\) por la derecha, entonces \(b = c\).

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

import Mathlib.Algebra.Group.Defs

variable {M : Type} [Monoid M]
variable {a b c : M}

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by sorry

5.1. Demostración en lenguaje natural

Por la siguiente cadena de igualdades \begin{align} b &= b * 1 &&\text{[por mul_one]} \newline &= b * (a * c) &&\text{[por hipótesis]} \newline &= (b * a) * c &&\text{[por mul_assoc]} \newline &= 1 * c &&\text{[por hipótesis]} \newline &= c &&\text{[por one_mul]} \newline \end{align}

5.2. Demostraciones con Lean4

import Mathlib.Algebra.Group.Defs

variable {M : Type} [Monoid M]
variable {a b c : M}

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
calc b = b * 1       := (mul_one b).symm
     _ = b * (a * c) := congrArg (b * .) hac.symm
     _ = (b * a) * c := (mul_assoc b a c).symm
     _ = 1 * c       := congrArg (. * c) hba
     _ = c           := one_mul c

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
calc b  = b * 1       := by aesop
      _ = b * (a * c) := by aesop
      _ = (b * a) * c := (mul_assoc b a c).symm
      _ = 1 * c       := by aesop
      _ = c           := by aesop

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by
  rw [←one_mul c]
  -- ⊢ b = 1 * c
  rw [←hba]
  -- ⊢ b = (b * a) * c
  rw [mul_assoc]
  -- ⊢ b = b * (a * c)
  rw [hac]
  -- ⊢ b = b * 1
  rw [mul_one b]

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]

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

example
  (hba : b * a = 1)
  (hac : a * c = 1)
  : b = c :=
left_inv_eq_right_inv hba hac

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

-- #check (left_inv_eq_right_inv : b * a = 1 → a * c = 1 → b = c)
-- #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.

5.3. Demostraciones con Isabelle/HOL

theory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "b * a = 1"
          "a * c = 1"
  shows   "b = c"
proof -
  have      "b  = b * 1"      by (simp only: right_neutral)
  also have "… = b * (a * c)" by (simp only: ‹a * c = 1›)
  also have "… = (b * a) * c" by (simp only: assoc)
  also have "… = 1 * c"       by (simp only: ‹b * a = 1›)
  also have "… = c"           by (simp only: left_neutral)
  finally show "b = c"        by this
qed

(* 2ª demostración *)

lemma
  assumes "b * a = 1"
          "a * c = 1"
  shows   "b = c"
proof -
  have      "b  = b * 1"      by simp
  also have "… = b * (a * c)" using ‹a * c = 1› by simp
  also have "… = (b * a) * c" by (simp add: assoc)
  also have "… = 1 * c"       using ‹b * a = 1› by simp
  also have "… = c"           by simp
  finally show "b = c"        by this
qed

(* 3ª demostración *)

lemma
  assumes "b * a = 1"
          "a * c = 1"
  shows   "b = c"
  using assms
  by (metis assoc left_neutral right_neutral)

end

end