Ir al contenido principal

La semana en Calculemus (23 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. Las funciones biyectivas tienen inversa

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

y que \(f\) tiene inversa por

   def tiene_inversa (f : X → Y) :=
     ∃ g, inversa f g

Demostrar con Lean4 que si la función \(f\) es biyectiva, entonces \(f\) tiene inversa.

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

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

example
  (hf : Bijective f)
  : tiene_inversa f :=
by sorry

1.1. Demostración en lenguaje natural

Sea \(f: X → Y\) biyectiva. Entonces, \(f\) es suprayectiva y se puede definir la función \(g: Y → X\) tal que \[ g(y) = x, \text{donde \(x\) es un elemento de \(X\) tal que \(f(x) = y\) \] Por tanto, \[ (∀y ∈ Y)[f(g(y)) = y] \tag{1} \]

Veamos que \(g\) es inversa de \(f\); es decir, que se verifican \begin{align} &(∀y ∈ Y)[(f ∘ g) y = y] \tag{2} \\ &(∀x ∈ X)[(g ∘ f) x = x] \tag{3} \end{align}

La propiedad (2) se tiene por (1) y la definición de composición.

Para demostrar (3), sea \(x ∈ X\). Entonces, por (1), \[ f(g(f(x))) = f(x) \] y, por ser f inyectiva, \[ g(f(x)) = x \] Luego, \[ (g ∘ f)(x) = x \]

1.2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

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

example
  (hf : Bijective f)
  : tiene_inversa f :=
by
  rcases hf with ⟨hfiny, hfsup⟩
  -- hfiny : Injective f
  -- hfsup : Surjective f
  choose g hg using hfsup
  -- g : Y → X
  -- hg : ∀ (b : Y), f (g b) = b
  use g
  -- ⊢ inversa g f
  constructor
  . -- ⊢ ∀ (x : Y), (f ∘ g) x = x
    exact hg
  . -- ⊢ ∀ (y : X), (g ∘ f) y = y
    intro a
    -- a : X
    -- ⊢ (g ∘ f) a = a
    rw [comp_apply]
    -- ⊢ g (f a) = a
    apply hfiny
    -- ⊢ f (g (f a)) = f a
    rw [hg (f a)]

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

example
  (hf : Bijective f)
  : tiene_inversa f :=
by
  rcases hf with ⟨hfiny, hfsup⟩
    -- hfiny : Injective f
    -- hfsup : Surjective f
  choose g hg using hfsup
  -- g : Y → X
  -- hg : ∀ (b : Y), f (g b) = b
  use g
  -- ⊢ inversa g f
  constructor
  . -- ⊢ ∀ (x : Y), (f ∘ g) x = x
    exact hg
  . -- ⊢ ∀ (y : X), (g ∘ f) y = y
    intro a
    -- a : X
    -- ⊢ (g ∘ f) a = a
    exact @hfiny (g (f a)) a (hg (f a))

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

example
  (hf : Bijective f)
  : tiene_inversa f :=
by
  rcases hf with ⟨hfiny, hfsup⟩
  -- hfiny : Injective f
  -- hfsup : Surjective f
  choose g hg using hfsup
  -- g : Y → X
  -- hg : ∀ (b : Y), f (g b) = b
  use g
  -- ⊢ inversa g f
  exact ⟨hg, fun a ↦ @hfiny (g (f a)) a (hg (f a))⟩

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

example
  (hf : Bijective f)
  : tiene_inversa f :=
by
  rcases hf with ⟨hfiny, hfsup⟩
  -- hfiny : Injective f
  -- hfsup : Surjective f
  choose g hg using hfsup
  -- g : Y → X
  -- hg : ∀ (b : Y), f (g b) = b
  exact ⟨g, ⟨hg, fun a ↦ @hfiny (g (f a)) a (hg (f a))⟩⟩

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

example
  (hf : Bijective f)
  : tiene_inversa f :=
by
  cases' (bijective_iff_has_inverse.mp hf) with g hg
  -- g : Y → X
  -- hg : LeftInverse g f ∧ Function.RightInverse g f
  aesop (add norm unfold [tiene_inversa, inversa])

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

-- variable (g : Y → X)
-- variable (x : X)
-- #check (bijective_iff_has_inverse : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f)
-- #check (comp_apply : (g ∘ f) x = g (f x))

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

1.3. Demostraciones con Isabelle/HOL

theory Las_funciones_biyectivas_tienen_inversa
imports Main
begin

definition inversa :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool" where
  "inversa f g ⟷ (∀ x. (g ∘ f) x = x) ∧ (∀ y. (f ∘ g) y = y)"

definition tiene_inversa :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa f ⟷ (∃ g. inversa f g)"

(* 1ª demostración *)

lemma
  assumes "bij f"
  shows   "tiene_inversa f"
proof -
  have "surj f"
    using assms by (rule bij_is_surj)
  then obtain g where hg : "∀y. f (g y) = y"
    by (metis surjD)
  have "inversa f g"
  proof (unfold inversa_def; intro conjI)
    show "∀x. (g ∘ f) x = x"
    proof (rule allI)
      fix x
      have "inj f"
        using ‹bij f› by (rule bij_is_inj)
      then show "(g ∘ f) x = x"
      proof (rule injD)
        have "f ((g ∘ f) x) = f (g (f x))"
          by simp
        also have "… = f x"
          by (simp add: hg)
        finally show "f ((g ∘ f) x) = f x"
          by this
      qed
    qed
    next
      show "∀y. (f ∘ g) y = y"
        by (simp add: hg)
  qed
  then show "tiene_inversa f"
    using tiene_inversa_def by blast
qed

(* 2ª demostración *)

lemma
  assumes "bij f"
  shows   "tiene_inversa f"
proof -
  have "surj f"
    using assms by (rule bij_is_surj)
  then obtain g where hg : "∀y. f (g y) = y"
    by (metis surjD)
  have "inversa f g"
  proof (unfold inversa_def; intro conjI)
    show "∀x. (g ∘ f) x = x"
    proof (rule allI)
      fix x
      have "inj f"
        using ‹bij f› by (rule bij_is_inj)
      then show "(g ∘ f) x = x"
      proof (rule injD)
        have "f ((g ∘ f) x) = f (g (f x))"
          by simp
        also have "… = f x"
          by (simp add: hg)
        finally show "f ((g ∘ f) x) = f x"
          by this
      qed
    qed
  next
    show "∀y. (f ∘ g) y = y"
      by (simp add: hg)
  qed
  then show "tiene_inversa f"
    using tiene_inversa_def by auto
qed

(* 3ª demostración *)

lemma
  assumes "bij f"
  shows   "tiene_inversa f"
proof -
  have "inversa f (inv f)"
  proof (unfold inversa_def; intro conjI)
    show "∀x. (inv f ∘ f) x = x"
      by (simp add: ‹bij f› bij_is_inj)
  next
    show "∀y. (f ∘ inv f) y = y"
      by (simp add: ‹bij f› bij_is_surj surj_f_inv_f)
  qed
  then show "tiene_inversa f"
    using tiene_inversa_def by auto
qed

end

2. La equipotencia es una relación reflexiva

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar que la relación de equipotencia es reflexiva.

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

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

example : Reflexive (. ⋍ .) :=
by sorry

2.1. Demostración en lenguaje natural

Tenemos que demostrar que para cualquier conjunto \(X\), se tiene que \(X\) es equipotente con \(X\). Para demostrarlo basta considerar que la función identidad en \(X\) es una biyección de \(X\) en \(X\).

2.2. Demostraciones con Lean4

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

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

example : Reflexive (. ⋍ .) :=
by
  intro X
  -- ⊢ X ⋍ X
  use id
  -- ⊢ Bijective id
  exact bijective_id

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

example : Reflexive (. ⋍ .) :=
by
  intro X
  -- ⊢ X ⋍ X
  exact ⟨id, bijective_id⟩

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

example : Reflexive (. ⋍ .) :=
fun _ ↦ ⟨id, bijective_id⟩

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

-- #check (bijective_id : Bijective id)

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

2.3. Demostraciones con Isabelle/HOL

theory La_equipotencia_es_una_relacion_reflexiva
imports Main "HOL-Library.Equipollence"
begin

(* 1ª demostración *)

lemma "reflp (≈)"
proof (rule reflpI)
  fix x :: "'a set"
  have "bij_betw id x x"
    by (simp only: bij_betw_id)
  then have "∃f. bij_betw f x x"
    by (simp only: exI)
  then show "x ≈ x"
    by (simp only: eqpoll_def)
qed

(* 2ª demostración *)

lemma "reflp (≈)"
by (simp only: reflpI eqpoll_refl)

(* 3ª demostración *)

lemma "reflp (≈)"
by (simp add: reflpI)

end

3. La inversa de una función es biyectiva

En Lean4 se puede definir que \(g\) es una inversa de \(f\) por

   def inversa (f : X → Y) (g : Y → X) :=
     (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

Demostrar que si \(g\) es una inversa de \(f\), entonces \(g\) es biyectiva.

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

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)
variable (g : Y → X)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

example
  (hg : inversa g f)
  : Bijective g :=
by sorry

3.1. Demostración en lenguaje natural

Para demostrar que \(g: Y → X\) es biyectiva, basta probar que existe una \(h\) que es inversa de \(g\) por la izquierda y por la derecha; es decir, \begin{align} &(∀y ∈ Y)[(h ∘ g)(y) = y] \tag{1} \newline &(∀x ∈ X)[(g ∘ h)(x) = x] \tag{2} \end{align}

Puesto que \(g\) es una inversa de \(f\), entonces \begin{align} &(∀x ∈ X)[(g ∘ f)(x) = x] \tag{3} \newline &(∀y ∈ Y)[(f ∘ g)(y) = y] \tag{4} \end{align}

Tomando \(f\) como \(h\), (1) se verifica por (4) y (2) se verifica por (3).

3.2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

variable {X Y : Type _}
variable (f : X → Y)
variable (g : Y → X)

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

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

example
  (hg : inversa g f)
  : Bijective g :=
by
  rcases hg with ⟨h1, h2⟩
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  use f
  -- ⊢ LeftInverse f g ∧ Function.RightInverse f g
  constructor
  . -- ⊢ LeftInverse f g
    exact h1
  . -- ⊢ Function.RightInverse f g
    exact h2

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

example
  (hg : inversa g f)
  : Bijective g :=
by
  rcases hg with ⟨h1, h2⟩
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  use f
  -- ⊢ LeftInverse f g ∧ Function.RightInverse f g
  exact ⟨h1, h2⟩

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

example
  (hg : inversa g f)
  : Bijective g :=
by
  rcases hg with ⟨h1, h2⟩
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, ⟨h1, h2⟩⟩

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

example
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  use f
  -- ⊢ LeftInverse f g ∧ Function.RightInverse f g
  exact hg

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

example
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

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

example
  (hg : inversa g f)
  : Bijective g :=
by
  apply bijective_iff_has_inverse.mpr
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

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

-- #check (bijective_iff_has_inverse : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f)

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

3.3. Demostraciones con Isabelle/HOL

theory La_inversa_de_una_funcion_biyectiva_es_biyectiva
imports Main
begin

definition inversa :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool" where
  "inversa f g ⟷ (∀ x. (g ∘ f) x = x) ∧ (∀ y. (f ∘ g) y = y)"

(* 1ª demostración *)

lemma
  fixes   f :: "'a ⇒ 'b"
  assumes "inversa g f"
  shows   "bij g"
proof (rule bijI)
  show "inj g"
  proof (rule injI)
    fix x y
    assume "g x = g y"
    have h1 : "∀ y. (f ∘ g) y = y"
      by (meson assms inversa_def)
    then have "x = (f ∘ g) x"
      by (simp only: allE)
    also have "… = f (g x)"
      by (simp only: o_apply)
    also have "… = f (g y)"
      by (simp only: ‹g x = g y›)
    also have "… = (f ∘ g) y"
      by (simp only: o_apply)
    also have "… = y"
      using h1 by (simp only: allE)
    finally show "x = y"
      by this
  qed
next
  show "surj g"
  proof (rule surjI)
    fix x
    have h2 : "∀ x. (g ∘ f) x = x"
      by (meson assms inversa_def)
    then have "(g ∘ f) x = x"
      by (simp only: allE)
    then show "g (f x) = x"
      by (simp only: o_apply)
  qed
qed

(* 2ª demostración *)

lemma
  fixes   f :: "'a ⇒ 'b"
  assumes "inversa g f"
  shows   "bij g"
proof (rule bijI)
  show "inj g"
  proof (rule injI)
    fix x y
    assume "g x = g y"
    have h1 : "∀ y. (f ∘ g) y = y"
      by (meson assms inversa_def)
    then show "x = y"
      by (metis ‹g x = g y› o_apply)
  qed
next
  show "surj g"
  proof (rule surjI)
    fix x
    have h2 : "∀ x. (g ∘ f) x = x"
      by (meson assms inversa_def)
    then show "g (f x) = x"
      by (simp only: o_apply)
  qed
qed

end

4. La equipotencia es una relación simétrica

Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por

   def es_equipotente (A B : Type _) : Prop :=
     ∃ g : A → B, Bijective g

   local infixr:50 " ⋍ " => es_equipotente

Demostrar con Lean4 que la relación de equipotencia es simétrica.

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

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

lemma aux1
  (hf : Bijective f)
  : tiene_inversa f :=
by
  cases' (bijective_iff_has_inverse.mp hf) with g hg
  -- g : Y → X
  -- hg : LeftInverse g f ∧ Function.RightInverse g f
  aesop (add norm unfold [tiene_inversa, inversa])

lemma aux2
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

example : Symmetric (. ⋍ .) :=
by sorry

4.1. Demostración en lenguaje natural

Sean \(A\) y \(B\) tales que \(A ⋍ B\). Entonces, existe \(f: A → B\) biyectiva. Por tanto, f tiene una inversa \(g: B → A\) que también es biyectiva. Luego, \(B ⋍ A\).

4.2. Demostraciones con Lean4

import Mathlib.Tactic

open Function

def es_equipotente (A B : Type _) : Prop :=
  ∃ g : A → B, Bijective g

local infixr:50 " ⋍ " => es_equipotente

def inversa (f : X → Y) (g : Y → X) :=
  (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)

def tiene_inversa (f : X → Y) :=
  ∃ g, inversa g f

lemma aux1
  (hf : Bijective f)
  : tiene_inversa f :=
by
  cases' (bijective_iff_has_inverse.mp hf) with g hg
  -- g : Y → X
  -- hg : LeftInverse g f ∧ Function.RightInverse g f
  aesop (add norm unfold [tiene_inversa, inversa])

lemma aux2
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

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

example : Symmetric (. ⋍ .) :=
by
  unfold Symmetric
  -- ⊢ ∀ ⦃x y : Type ?u.17753⦄, (fun x x_1 => x ⋍ x_1) x y → (fun x x_1 => x ⋍ x_1) y x
  intros x y hxy
  -- x y : Type ?u.17753
  -- hxy : x ⋍ y
  -- ⊢ y ⋍ x
  unfold es_equipotente at *
  -- hxy : ∃ g, Bijective g
  -- ⊢ ∃ g, Bijective g
  cases' hxy with f hf
  -- f : x → y
  -- hf : Bijective f
  have h1 : tiene_inversa f := aux1 hf
  cases' h1 with g hg
  -- g : y → x
  -- hg : inversa g f
  use g
  -- ⊢ Bijective g
  exact aux2 hg

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

example : Symmetric (. ⋍ .) :=
by
  intros x y hxy
  -- x y : Type ?u.17965
  -- hxy : x ⋍ y
  -- ⊢ y ⋍ x
  cases' hxy with f hf
  -- f : x → y
  -- hf : Bijective f
  cases' (aux1 hf) with g hg
  -- g : y → x
  -- hg : inversa g f
  exact ⟨g, aux2 hg⟩

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

example : Symmetric (. ⋍ .) :=
by
  rintro x y ⟨f, hf⟩
  -- x y : Type ?u.18159
  -- f : x → y
  -- hf : Bijective f
  -- ⊢ y ⋍ x
  cases' (aux1 hf) with g hg
  -- g : y → x
  -- hg : inversa g f
  exact ⟨g, aux2 hg⟩

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

-- variable (α β : Type _)
-- variable (f : α → β)
-- #check (bijective_iff_has_inverse : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f)

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

4.3. Demostraciones con Isabelle/HOL

theory La_equipotencia_es_una_relacion_simetrica
imports Main "HOL-Library.Equipollence"
begin

(* 1ª demostración *)

lemma "symp (≈)"
proof (rule sympI)
  fix x y :: "'a set"
  assume "x ≈ y"
  then obtain f where "bij_betw f x y"
    using eqpoll_def by blast
  then have "bij_betw (the_inv_into x f) y x"
    by (rule bij_betw_the_inv_into)
  then have "∃g. bij_betw g y x"
    by auto
  then show "y ≈ x"
    by (simp only: eqpoll_def)
qed

(* 2ª demostración *)

lemma "symp (≈)"
  unfolding eqpoll_def symp_def
  using bij_betw_the_inv_into by auto

(* 3ª demostración *)

lemma "symp (≈)"
  by (simp add: eqpoll_sym sympI)

end

5. La composición de funciones biyectivas es biyectiva

Demostrar con Lean4 que la composición de dos funciones biyectivas es una función biyectiva.

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
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by sorry

5.1. Demostración en lenguaje natural

Sean \(f: X → Y\) y \(g: Y → Z\). En ejercicios anteriores hemos demostrados los siguientes lemas:

  • Lema 1: Si \(f\) y \(g\) son inyectiva, entonces también lo es \(g ∘ f\).
  • Lema 2: Si \(f\) y \(g\) son suprayectiva, entonces también lo es \(g ∘ f\).

Supongamos que \(f\) y \(g\) son biyectivas. Entonces, son inyectivas y suprayectivas. Luego, por los lemas 1 y 2, \(g ∘ f\) es inyectiva y suprayectiva. Por tanto, \(g ∘ f\) es biyectiva.

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
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by
  cases' Hf with Hfi Hfs
  -- Hfi : Injective f
  -- Hfs : Surjective f
  cases' Hg with Hgi Hgs
  -- Hgi : Injective g
  -- Hgs : Surjective g
  constructor
  . -- ⊢ Injective (g ∘ f)
    apply Injective.comp
    . -- ⊢ Injective g
      exact Hgi
    . -- ⊢ Injective f
      exact Hfi
  . apply Surjective.comp
    . -- ⊢ Surjective g
      exact Hgs
    . -- ⊢ Surjective f
      exact Hfs

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

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by
  cases' Hf with Hfi Hfs
  -- Hfi : Injective f
  -- Hfs : Surjective f
  cases' Hg with Hgi Hgs
  -- Hgi : Injective g
  -- Hgs : Surjective g
  constructor
  . -- ⊢ Injective (g ∘ f)
    exact Injective.comp Hgi Hfi
  . -- ⊢ Surjective (g ∘ f)
    exact Surjective.comp Hgs Hfs

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

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
by
  cases' Hf with Hfi Hfs
  -- Hfi : Injective f
  -- Hfs : Surjective f
  cases' Hg with Hgi Hgs
  -- Hgi : Injective g
  -- Hgs : Surjective g
  exact ⟨Injective.comp Hgi Hfi,
         Surjective.comp Hgs Hfs⟩

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

example :
  Bijective f → Bijective g → Bijective (g ∘ f) :=
by
  rintro ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩
  -- Hfi : Injective f
  -- Hfs : Surjective f
  -- Hgi : Injective g
  -- Hgs : Surjective g
  exact ⟨Injective.comp Hgi Hfi,
         Surjective.comp Hgs Hfs⟩

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

example :
  Bijective f → Bijective g → Bijective (g ∘ f) :=
fun ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩ ↦ ⟨Injective.comp Hgi Hfi,
                             Surjective.comp Hgs Hfs⟩

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

example
  (Hf : Bijective f)
  (Hg : Bijective g)
  : Bijective (g ∘ f) :=
Bijective.comp Hg Hf

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

-- #check (Bijective.comp : Bijective g → Bijective f → Bijective (g ∘ f))
-- #check (Injective.comp : Injective g → Injective f → Injective (g ∘ f))
-- #check (Surjective.comp : Surjective g → Surjective f → Surjective (g ∘ f))

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

5.3. Demostraciones con Isabelle/HOL

theory La_composicion_de_funciones_biyectivas_es_biyectiva
imports Main
begin

(* 1ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
proof (rule bijI)
  show "inj (g ∘ f)"
  proof (rule inj_compose)
    show "inj g"
      using ‹bij g› by (rule bij_is_inj)
  next
    show "inj f"
      using ‹bij f› by (rule bij_is_inj)
  qed
next
  show "surj (g ∘ f)"
  proof (rule comp_surj)
    show "surj f"
      using ‹bij f› by (rule bij_is_surj)
  next
    show "surj g"
      using ‹bij g› by (rule bij_is_surj)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
proof (rule bijI)
  show "inj (g ∘ f)"
  proof (rule inj_compose)
    show "inj g"
      by (rule bij_is_inj [OF ‹bij g›])
  next
    show "inj f"
      by (rule bij_is_inj [OF ‹bij f›])
  qed
next
  show "surj (g ∘ f)"
  proof (rule comp_surj)
    show "surj f"
      by (rule bij_is_surj [OF ‹bij f›])
  next
    show "surj g"
      by (rule bij_is_surj [OF ‹bij g›])
  qed
qed

(* 3ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
proof (rule bijI)
  show "inj (g ∘ f)"
    by (rule inj_compose [OF bij_is_inj [OF ‹bij g›]
                             bij_is_inj [OF ‹bij f›]])
next
  show "surj (g ∘ f)"
    by (rule comp_surj [OF bij_is_surj [OF ‹bij f›]
                           bij_is_surj [OF ‹bij g›]])
qed

(* 4ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
by (rule bijI [OF inj_compose [OF bij_is_inj  [OF ‹bij g›]
                                  bij_is_inj  [OF ‹bij f›]]
                  comp_surj   [OF bij_is_surj [OF ‹bij f›]
                                  bij_is_surj [OF ‹bij g›]]])

(* 5ª demostración *)

lemma
  assumes "bij f"
          "bij g"
  shows   "bij (g ∘ f)"
using assms
by (rule bij_comp)

(* Nota: Auto solve indica la demostración anterior. *)

end