José A. Alonso

La igualdad de valores es una relación de equivalencia

PorJosé A. Alonso 19 agosto 202110 agosto 2021

Sean X e Y dos conjuntos y f una función de X en Y. Se define la relación R en X de forma que x está relacionado con y si f(x) = f(y).

Demostrar que R es una relación de equivalencia.

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

import tactic

universe u
variables {X Y : Type u}
variable  (f : X → Y)

def R (x y : X) := f x = f y

example : equivalence (R f) :=
sorry

import tactic

universe u

variables {X Y : Type u}

variable (f : X → Y)

def R (x y : X) := f x = f y

example : equivalence (R f) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

universe u
variables {X Y : Type u}
variable  (f : X → Y)

def R (x y : X) := f x = f y

-- 1ª demostración
example : equivalence (R f) :=
begin
  unfold equivalence,
  repeat { split },
  { unfold reflexive,
    intro x,
    unfold R, },
  { unfold symmetric,
    intros x y hxy,
    unfold R,
    exact symm hxy, },
  { unfold transitive,
    unfold R,
    intros x y z hxy hyz,
    exact eq.trans hxy hyz, },
end

-- 2ª demostración
example : equivalence (R f) :=
begin
  repeat { split },
  { intro x,
    exact rfl, },
  { intros x y hxy,
    exact eq.symm hxy, },
  { intros x y z hxy hyz,
    exact eq.trans hxy hyz, },
end

-- 3ª demostración
example : equivalence (R f) :=
begin
  repeat { split },
  { exact λ x, rfl, },
  { exact λ x y hxy, eq.symm hxy, },
  { exact λ x y z hxy hyz, eq.trans hxy hyz, },
end

-- 4ª demostración
example : equivalence (R f) :=
⟨λ x, rfl,
 λ x y hxy, eq.symm hxy,
 λ x y z hxy hyz, eq.trans hxy hyz⟩

import tactic

universe u

variables {X Y : Type u}

variable (f : X → Y)

def R (x y : X) := f x = f y

-- 1ª demostración

example : equivalence (R f) :=

begin

unfold equivalence,

repeat { split },

{ unfold reflexive,

intro x,

unfold R, },

{ unfold symmetric,

intros x y hxy,

unfold R,

exact symm hxy, },

{ unfold transitive,

unfold R,

intros x y z hxy hyz,

exact eq.trans hxy hyz, },

end

-- 2ª demostración

example : equivalence (R f) :=

begin

repeat { split },

{ intro x,

exact rfl, },

{ intros x y hxy,

exact eq.symm hxy, },

{ intros x y z hxy hyz,

exact eq.trans hxy hyz, },

end

-- 3ª demostración

example : equivalence (R f) :=

begin

repeat { split },

{ exact λ x, rfl, },

{ exact λ x y hxy, eq.symm hxy, },

{ exact λ x y z hxy hyz, eq.trans hxy hyz, },

end

-- 4ª demostración

example : equivalence (R f) :=

⟨λ x, rfl,

λ x y hxy, eq.symm hxy,

λ x y z hxy hyz, eq.trans hxy hyz⟩

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory La_igualdad_de_valores_es_una_relacion_de_equivalencia
imports Main
begin

definition R :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where
  "R f x y ⟷ (f x = f y)"

(* 1ª demostración *)
lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
  proof (rule reflpI)
    fix x
    have "f x = f x"
      by (rule refl)
    then show "R f x x"
      by (unfold R_def)
  qed
next
  show "symp (R f)"
  proof (rule sympI)
    fix x y
    assume "R f x y"
    then have "f x = f y"
      by (unfold R_def)
    then have "f y = f x"
      by (rule sym)
    then show "R f y x"
      by (unfold R_def)
  qed
next
  show "transp (R f)"
  proof (rule transpI)
    fix x y z
    assume "R f x y" and "R f y z"
    then have "f x = f y" and "f y = f z"
      by (unfold R_def)
    then have "f x = f z"
      by (rule ssubst)
    then show "R f x z"
      by (unfold R_def)
  qed
qed

(* 2ª demostración *)
lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
  proof (rule reflpI)
    fix x
    show "R f x x"
      by (metis R_def)
  qed
next
  show "symp (R f)"
  proof (rule sympI)
    fix x y
    assume "R f x y"
    then show "R f y x"
      by (metis R_def)
  qed
next
  show "transp (R f)"
  proof (rule transpI)
    fix x y z
    assume "R f x y" and "R f y z"
    then show "R f x z"
      by (metis R_def)
  qed
qed

(* 3ª demostración *)
lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
    by (simp add: R_def reflpI)
next
  show "symp (R f)"
    by (metis R_def sympI)
next
  show "transp (R f)"
    by (metis R_def transpI)
qed

(* 4ª demostración *)
lemma "equivp (R f)"
  by (metis R_def
            equivpI
            reflpI
            sympI
            transpI)

end

theory La_igualdad_de_valores_es_una_relacion_de_equivalencia

imports Main

begin

definition R :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where

"R f x y ⟷ (f x = f y)"

(* 1ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

proof (rule reflpI)

fix x

have "f x = f x"

by (rule refl)

then show "R f x x"

by (unfold R_def)

qed

show "symp (R f)"

proof (rule sympI)

fix x y

assume "R f x y"

then have "f x = f y"

by (unfold R_def)

then have "f y = f x"

by (rule sym)

then show "R f y x"

by (unfold R_def)

qed

show "transp (R f)"

proof (rule transpI)

fix x y z

assume "R f x y" and "R f y z"

then have "f x = f y" and "f y = f z"

by (unfold R_def)

then have "f x = f z"

by (rule ssubst)

then show "R f x z"

by (unfold R_def)

qed

(* 2ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

proof (rule reflpI)

fix x

show "R f x x"

by (metis R_def)

qed

show "symp (R f)"

proof (rule sympI)

fix x y

assume "R f x y"

then show "R f y x"

by (metis R_def)

qed

show "transp (R f)"

proof (rule transpI)

fix x y z

assume "R f x y" and "R f y z"

then show "R f x z"

by (metis R_def)

qed

(* 3ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

by (simp add: R_def reflpI)

show "symp (R f)"

by (metis R_def sympI)

show "transp (R f)"

by (metis R_def transpI)

qed

(* 4ª demostración *)

lemma "equivp (R f)"

by (metis R_def

equivpI

reflpI

sympI

transpI)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La equipotencia es una relación de equivalencia

PorJosé A. Alonso 18 agosto 20216 agosto 2021

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*) :=
     ∃ g : A → B, bijective g

   infix ` ⋍ `: 50 := es_equipotente

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

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

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

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

example : equivalence (⋍) :=
sorry

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

example : equivalence (⋍) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

variables {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)

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

lemma aux1
  (hf : bijective f)
  : tiene_inversa f :=
begin
  cases (bijective_iff_has_inverse.mp hf) with g hg,
  by tidy,
end

lemma aux2
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
bijective_iff_has_inverse.mpr (by use [f, hg])

example : equivalence (⋍) :=
begin
  repeat {split},
  { exact λ X, ⟨id, bijective_id⟩ },
  { rintros X Y ⟨f, hf⟩,
    cases (aux1 hf) with g hg,
    use [g, aux2 hf hg], },
  { rintros X Y Z ⟨f, hf⟩ ⟨g, hg⟩,
    exact ⟨g ∘ f, bijective.comp hg hf⟩, },
end

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

variables {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)

def tiene_inversa (f : X → Y) :=

∃ g, inversa g f

lemma aux1

(hf : bijective f)

: tiene_inversa f :=

begin

cases (bijective_iff_has_inverse.mp hf) with g hg,

by tidy,

end

lemma aux2

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

bijective_iff_has_inverse.mpr (by use [f, hg])

example : equivalence (⋍) :=

begin

repeat {split},

{ exact λ X, ⟨id, bijective_id⟩ },

{ rintros X Y ⟨f, hf⟩,

cases (aux1 hf) with g hg,

use [g, aux2 hf hg], },

{ rintros X Y Z ⟨f, hf⟩ ⟨g, hg⟩,

exact ⟨g ∘ f, bijective.comp hg hf⟩, },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

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

(* 1ª demostración *)
lemma "equivp (≈)"
proof (rule equivpI)
  show "reflp (≈)"
    using reflpI eqpoll_refl by blast
next
  show "symp (≈)"
    using sympI eqpoll_sym by blast
next
  show "transp (≈)"
    using transpI eqpoll_trans by blast
qed

(* 2ª demostración *)
lemma "equivp (≈)"
  by (simp add: equivp_reflp_symp_transp
                reflpI
                sympI
                eqpoll_sym
                transpI
                eqpoll_trans)

end

theory La_equipotencia_es_una_relacion_de_equivalencia

imports Main "HOL-Library.Equipollence"

begin

(* 1ª demostración *)

lemma "equivp (≈)"

proof (rule equivpI)

show "reflp (≈)"

using reflpI eqpoll_refl by blast

show "symp (≈)"

using sympI eqpoll_sym by blast

show "transp (≈)"

using transpI eqpoll_trans by blast

qed

(* 2ª demostración *)

lemma "equivp (≈)"

by (simp add: equivp_reflp_symp_transp

reflpI

sympI

eqpoll_sym

transpI

eqpoll_trans)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La equipotencia es una relación transitiva

PorJosé A. Alonso 17 agosto 20216 agosto 2021

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*) :=
     ∃ g : A → B, bijective g

   infix ` ⋍ `: 50 := es_equipotente

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

Demostrar que la relación de equipotencia es transitiva.

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

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

example : transitive (⋍) :=
sorry

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

example : transitive (⋍) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

-- 1ª demostración
example : transitive (⋍) :=
begin
  intros X Y Z hXY hYZ,
  unfold es_equipotente at *,
  cases hXY with f hf,
  cases hYZ with g hg,
  use (g ∘ f),
  exact bijective.comp hg hf,
end

-- 2ª demostración
example : transitive (⋍) :=
begin
  rintros X Y Z ⟨f, hf⟩ ⟨g, hg⟩,
  use [g ∘ f, bijective.comp hg hf],
end

-- 3ª demostración
example : transitive (⋍) :=
λ X Y Z ⟨f, hf⟩ ⟨g, hg⟩, by use [g ∘ f, bijective.comp hg hf]

-- 4ª demostración
example : transitive (⋍) :=
λ X Y Z ⟨f, hf⟩ ⟨g, hg⟩, exists.intro (g ∘ f) (bijective.comp hg hf)

-- 4ª demostración
example : transitive (⋍) :=
λ X Y Z ⟨f, hf⟩ ⟨g, hg⟩, ⟨g ∘ f, bijective.comp hg hf⟩

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

-- 1ª demostración

example : transitive (⋍) :=

begin

intros X Y Z hXY hYZ,

unfold es_equipotente at *,

cases hXY with f hf,

cases hYZ with g hg,

use (g ∘ f),

exact bijective.comp hg hf,

end

-- 2ª demostración

example : transitive (⋍) :=

begin

rintros X Y Z ⟨f, hf⟩ ⟨g, hg⟩,

use [g ∘ f, bijective.comp hg hf],

end

-- 3ª demostración

example : transitive (⋍) :=

λ X Y Z ⟨f, hf⟩ ⟨g, hg⟩, by use [g ∘ f, bijective.comp hg hf]

-- 4ª demostración

example : transitive (⋍) :=

λ X Y Z ⟨f, hf⟩ ⟨g, hg⟩, exists.intro (g ∘ f) (bijective.comp hg hf)

-- 4ª demostración

example : transitive (⋍) :=

λ X Y Z ⟨f, hf⟩ ⟨g, hg⟩, ⟨g ∘ f, bijective.comp hg hf⟩

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

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

(* 1ª demostración *)
lemma "transp (≈)"
proof (rule transpI)
  fix x y z :: "'a set"
  assume "x ≈ y" and "y ≈ z"
  show "x ≈ z"
  proof (unfold eqpoll_def)
    obtain f where hf : "bij_betw f x y"
      using ‹x ≈ y› eqpoll_def by auto
    obtain g where hg : "bij_betw g y z"
      using ‹y ≈ z› eqpoll_def by auto
    have "bij_betw (g ∘ f) x z"
      using hf hg by (rule bij_betw_trans)
    then show "∃h. bij_betw h x z"
      by auto
  qed
qed

(* 2ª demostración *)
lemma "transp (≈)"
  unfolding eqpoll_def transp_def
  by (meson bij_betw_trans)

(* 3ª demostración *)
lemma "transp (≈)"
  by (simp add: eqpoll_trans transpI)

end

theory La_equipotencia_es_una_relacion_transitiva

imports Main "HOL-Library.Equipollence"

begin

(* 1ª demostración *)

lemma "transp (≈)"

proof (rule transpI)

fix x y z :: "'a set"

assume "x ≈ y" and "y ≈ z"

show "x ≈ z"

proof (unfold eqpoll_def)

obtain f where hf : "bij_betw f x y"

using ‹x ≈ y› eqpoll_def by auto

obtain g where hg : "bij_betw g y z"

using ‹y ≈ z› eqpoll_def by auto

have "bij_betw (g ∘ f) x z"

using hf hg by (rule bij_betw_trans)

then show "∃h. bij_betw h x z"

by auto

qed

(* 2ª demostración *)

lemma "transp (≈)"

unfolding eqpoll_def transp_def

by (meson bij_betw_trans)

(* 3ª demostración *)

lemma "transp (≈)"

by (simp add: eqpoll_trans transpI)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La composición de funciones biyectivas es biyectiva

PorJosé A. Alonso 16 agosto 20216 agosto 2021

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

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

import tactic
open function

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

example
  (Hf : bijective f)
  (Hg : bijective g)
  : bijective (g ∘ f) :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(Hf : bijective f)

(Hg : bijective g)

: bijective (g ∘ f) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

variables {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) :=
begin
  cases Hf with Hfi Hfs,
  cases Hg with Hgi Hgs,
  split,
  { apply injective.comp,
    { exact Hgi, },
    { exact Hfi, }},
  { apply surjective.comp,
    { exact Hgs, },
    { exact Hfs, }},
end

-- 2ª demostración
example
  (Hf : bijective f)
  (Hg : bijective g)
  : bijective (g ∘ f) :=
begin
  cases Hf with Hfi Hfs,
  cases Hg with Hgi Hgs,
  split,
  { exact injective.comp Hgi Hfi, },
  { exact surjective.comp Hgs Hfs, },
end

-- 3ª demostración
example
  (Hf : bijective f)
  (Hg : bijective g)
  : bijective (g ∘ f) :=
begin
  cases Hf with Hfi Hfs,
  cases Hg with Hgi Hgs,
  exact ⟨injective.comp Hgi Hfi,
         surjective.comp Hgs Hfs⟩,
end

-- 4ª demostración
example :
  bijective f → bijective g → bijective (g ∘ f) :=
begin
  rintros ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩,
  exact ⟨injective.comp Hgi Hfi,
         surjective.comp Hgs Hfs⟩,
end

-- 5ª demostración
example :
  bijective f → bijective g → bijective (g ∘ f) :=
λ ⟨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) :=
-- by library_search
bijective.comp Hg Hf

import tactic

open function

variables {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) :=

begin

cases Hf with Hfi Hfs,

cases Hg with Hgi Hgs,

split,

{ apply injective.comp,

{ exact Hgi, },

{ exact Hfi, }},

{ apply surjective.comp,

{ exact Hgs, },

{ exact Hfs, }},

end

-- 2ª demostración

example

(Hf : bijective f)

(Hg : bijective g)

: bijective (g ∘ f) :=

begin

cases Hf with Hfi Hfs,

cases Hg with Hgi Hgs,

split,

{ exact injective.comp Hgi Hfi, },

{ exact surjective.comp Hgs Hfs, },

end

-- 3ª demostración

example

(Hf : bijective f)

(Hg : bijective g)

: bijective (g ∘ f) :=

begin

cases Hf with Hfi Hfs,

cases Hg with Hgi Hgs,

exact ⟨injective.comp Hgi Hfi,

surjective.comp Hgs Hfs⟩,

end

-- 4ª demostración

example :

bijective f → bijective g → bijective (g ∘ f) :=

begin

rintros ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩,

exact ⟨injective.comp Hgi Hfi,

surjective.comp Hgs Hfs⟩,

end

-- 5ª demostración

example :

bijective f → bijective g → bijective (g ∘ f) :=

λ ⟨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) :=

-- by library_search

bijective.comp Hg Hf

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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)

end

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)

show "inj f"

using ‹bij f› by (rule bij_is_inj)

qed

show "surj (g ∘ f)"

proof (rule comp_surj)

show "surj f"

using ‹bij f› by (rule bij_is_surj)

show "surj g"

using ‹bij g› by (rule bij_is_surj)

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›])

show "inj f"

by (rule bij_is_inj [OF ‹bij f›])

qed

show "surj (g ∘ f)"

proof (rule comp_surj)

show "surj f"

by (rule bij_is_surj [OF ‹bij f›])

show "surj g"

by (rule bij_is_surj [OF ‹bij g›])

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›]])

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)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La composición de funciones suprayectivas es suprayectiva

PorJosé A. Alonso 15 agosto 20216 agosto 2021

Demostrar que la composición de dos funciones suprayectivas es una función suprayectiva.

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

import tactic
open function

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

example
  (hf : surjective f)
  (hg : surjective g)
  : surjective (g ∘ f) :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(hf : surjective f)

(hg : surjective g)

: surjective (g ∘ f) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

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

-- 1ª demostración
example
  (hf : surjective f)
  (hg : surjective g)
  : surjective (g ∘ f) :=
begin
  intro z,
  cases hg z with y hy,
  cases hf y with x hx,
  use x,
  dsimp,
  rw hx,
  exact hy,
end

-- 2ª demostración
example
  (hf : surjective f)
  (hg : surjective g)
  : surjective (g ∘ f) :=
begin
  intro z,
  cases hg z with y hy,
  cases hf y with x hx,
  use x,
  calc (g ∘ f) x = g (f x) : by rw comp_app
             ... = g y     : congr_arg g hx
             ... = z       : hy,
end

-- 3ª demostración
example
  (hf : surjective f)
  (hg : surjective g)
  : surjective (g ∘ f) :=
assume z,
exists.elim (hg z)
  ( assume y (hy : g y = z),
    exists.elim (hf y)
    ( assume x (hx : f x = y),
      have g (f x) = z, from eq.subst (eq.symm hx) hy,
      show ∃ x, g (f x) = z, from exists.intro x this))

-- 4ª demostración
example
  (hf : surjective f)
  (hg : surjective g)
  : surjective (g ∘ f) :=
-- by library_search
surjective.comp hg hf

-- 5ª demostración
example
  (hf : surjective f)
  (hg : surjective g)
  : surjective (g ∘ f) :=
λ z, exists.elim (hg z)
  (λ y hy, exists.elim (hf y)
     (λ x hx, exists.intro x
        (show g (f x) = z,
           from (eq.trans (congr_arg g hx) hy))))

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

-- 1ª demostración

example

(hf : surjective f)

(hg : surjective g)

: surjective (g ∘ f) :=

begin

intro z,

cases hg z with y hy,

cases hf y with x hx,

use x,

dsimp,

rw hx,

exact hy,

end

-- 2ª demostración

example

(hf : surjective f)

(hg : surjective g)

: surjective (g ∘ f) :=

begin

intro z,

cases hg z with y hy,

cases hf y with x hx,

use x,

calc (g ∘ f) x = g (f x) : by rw comp_app

... = g y : congr_arg g hx

... = z : hy,

end

-- 3ª demostración

example

(hf : surjective f)

(hg : surjective g)

: surjective (g ∘ f) :=

assume z,

exists.elim (hg z)

( assume y (hy : g y = z),

exists.elim (hf y)

( assume x (hx : f x = y),

have g (f x) = z, from eq.subst (eq.symm hx) hy,

show ∃ x, g (f x) = z, from exists.intro x this))

-- 4ª demostración

example

(hf : surjective f)

(hg : surjective g)

: surjective (g ∘ f) :=

-- by library_search

surjective.comp hg hf

-- 5ª demostración

example

(hf : surjective f)

(hg : surjective g)

: surjective (g ∘ f) :=

λ z, exists.elim (hg z)

(λ y hy, exists.elim (hf y)

(λ x hx, exists.intro x

(show g (f x) = z,

from (eq.trans (congr_arg g hx) hy))))

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory La_composicion_de_funciones_suprayectivas_es_suprayectiva
imports Main
begin

(* 1ª demostración *)
lemma
  assumes "surj (f :: 'a ⇒ 'b)"
          "surj (g :: 'b ⇒ 'c)"
  shows   "surj (g ∘ f)"
proof (unfold surj_def; intro allI)
  fix z
  obtain y where hy : "g y = z"
    using ‹surj g› by (metis surjD)
  obtain x where hx : "f x = y"
    using ‹surj f› by (metis surjD)
  have "(g ∘ f) x = g (f x)"
    by (simp only: o_apply)
  also have "… = g y"
    by (simp only: ‹f x = y›)
  also have "… = z"
    by (simp only: ‹g y = z›)
  finally have "(g ∘ f) x = z"
    by this
  then have "z = (g ∘ f) x"
    by (rule sym)
  then show "∃x. z = (g ∘ f) x"
    by (rule exI)
qed

(* 2ª demostración *)
lemma
  assumes "surj f"
          "surj g"
  shows   "surj (g ∘ f)"
using assms image_comp [of g f UNIV]
by (simp only:)

(* 3ª demostración *)
lemma
  assumes "surj f"
          "surj g"
  shows   "surj (g ∘ f)"
using assms
by (rule comp_surj)

end

theory La_composicion_de_funciones_suprayectivas_es_suprayectiva

imports Main

begin

(* 1ª demostración *)

lemma

assumes "surj (f :: 'a ⇒ 'b)"

"surj (g :: 'b ⇒ 'c)"

shows "surj (g ∘ f)"

proof (unfold surj_def; intro allI)

fix z

obtain y where hy : "g y = z"

using ‹surj g› by (metis surjD)

obtain x where hx : "f x = y"

using ‹surj f› by (metis surjD)

have "(g ∘ f) x = g (f x)"

by (simp only: o_apply)

also have "… = g y"

by (simp only: ‹f x = y›)

also have "… = z"

by (simp only: ‹g y = z›)

finally have "(g ∘ f) x = z"

by this

then have "z = (g ∘ f) x"

by (rule sym)

then show "∃x. z = (g ∘ f) x"

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "surj f"

"surj g"

shows "surj (g ∘ f)"

using assms image_comp [of g f UNIV]

by (simp only:)

(* 3ª demostración *)

lemma

assumes "surj f"

"surj g"

shows "surj (g ∘ f)"

using assms

by (rule comp_surj)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La composición de funciones inyectivas es inyectiva

PorJosé A. Alonso 14 agosto 202121 agosto 2021

Demostrar que la composición de dos funciones inyectivas es una función inyectiva.

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

import tactic
open function

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

example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

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

-- 1ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
begin
  intros x y h,
  apply Hf,
  apply Hg,
  exact h,
end

-- 2ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
begin
  intros x y h,
  apply Hf,
  exact Hg h,
end

-- 3ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
begin
  intros x y h,
  exact Hf (Hg h),
end

-- 4ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
λ x y h, Hf (Hg h)

-- 5ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
assume x y,
assume h1 : (g ∘ f) x = (g ∘ f) y,
have h2 : f x = f y, from Hg h1,
show x = y, from Hf h2

-- 6ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
assume x y,
assume h1 : (g ∘ f) x = (g ∘ f) y,
show x = y, from Hf (Hg h1)

-- 7ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
assume x y,
assume h1 : (g ∘ f) x = (g ∘ f) y,
Hf (Hg h1)

-- 8ª demostración
example
  (Hf : injective f)
  (Hg : injective g)
  : injective (g ∘ f) :=
λ x y h1, Hf (Hg h1)

-- 9ª demostración
example
  (Hg : injective g)
  (Hf : injective f)
  : injective (g ∘ f) :=
-- by library_search
injective.comp Hg Hf

-- 10ª demostración
example
  (Hg : injective g)
  (Hf : injective f)
  : injective (g ∘ f) :=
-- by hint
by tauto

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

-- 1ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

begin

intros x y h,

apply Hf,

apply Hg,

exact h,

end

-- 2ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

begin

intros x y h,

apply Hf,

exact Hg h,

end

-- 3ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

begin

intros x y h,

exact Hf (Hg h),

end

-- 4ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

λ x y h, Hf (Hg h)

-- 5ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

assume x y,

assume h1 : (g ∘ f) x = (g ∘ f) y,

have h2 : f x = f y, from Hg h1,

show x = y, from Hf h2

-- 6ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

assume x y,

assume h1 : (g ∘ f) x = (g ∘ f) y,

show x = y, from Hf (Hg h1)

-- 7ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

assume x y,

assume h1 : (g ∘ f) x = (g ∘ f) y,

Hf (Hg h1)

-- 8ª demostración

example

(Hf : injective f)

(Hg : injective g)

: injective (g ∘ f) :=

λ x y h1, Hf (Hg h1)

-- 9ª demostración

example

(Hg : injective g)

(Hf : injective f)

: injective (g ∘ f) :=

-- by library_search

injective.comp Hg Hf

-- 10ª demostración

example

(Hg : injective g)

(Hf : injective f)

: injective (g ∘ f) :=

-- by hint

by tauto

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory La_composicion_de_funciones_inyectivas_es_inyectiva
imports Main
begin

(* 1ª demostración *)
lemma
  assumes "inj f"
          "inj g"
  shows   "inj (f ∘ g)"
proof (rule injI)
  fix x y
  assume "(f ∘ g) x = (f ∘ g) y"
  then have "f (g x) = f (g y)"
    by (simp only: o_apply)
  then have "g x = g y"
    using ‹inj f› by (simp only: injD)
  then show "x = y"
    using ‹inj g› by (simp only: injD)
qed

(* 2ª demostración *)
lemma
  assumes "inj f"
          "inj g"
  shows   "inj (f ∘ g)"
using assms
by (simp add: inj_def)

(* 3ª demostración *)
lemma
  assumes "inj f"
          "inj g"
  shows   "inj (f ∘ g)"
using assms
by (rule inj_compose)

end

theory La_composicion_de_funciones_inyectivas_es_inyectiva

imports Main

begin

(* 1ª demostración *)

lemma

assumes "inj f"

"inj g"

shows "inj (f ∘ g)"

proof (rule injI)

fix x y

assume "(f ∘ g) x = (f ∘ g) y"

then have "f (g x) = f (g y)"

by (simp only: o_apply)

then have "g x = g y"

using ‹inj f› by (simp only: injD)

then show "x = y"

using ‹inj g› by (simp only: injD)

qed

(* 2ª demostración *)

lemma

assumes "inj f"

"inj g"

shows "inj (f ∘ g)"

using assms

by (simp add: inj_def)

(* 3ª demostración *)

lemma

assumes "inj f"

"inj g"

shows "inj (f ∘ g)"

using assms

by (rule inj_compose)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La equipotencia es una relación simétrica

PorJosé A. Alonso 13 agosto 20215 agosto 2021

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*) :=
     ∃ g : A → B, bijective g

   infix ` ⋍ `: 50 := es_equipotente

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

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

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

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

variables {X Y : Type*}
variable  {f : X → Y}
variable  {g : Y → X}

example : symmetric (⋍) :=
sorry

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

variables {X Y : Type*}

variable {f : X → Y}

variable {g : Y → X}

example : symmetric (⋍) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

variables {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)

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

lemma aux1
  (hf : bijective f)
  : tiene_inversa f :=
begin
  cases (bijective_iff_has_inverse.mp hf) with g hg,
  by tidy,
end

lemma aux2
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
bijective_iff_has_inverse.mpr (by use [f, hg])

-- 1ª demostración
example : symmetric (⋍) :=
begin
  unfold symmetric,
  intros x y hxy,
  unfold es_equipotente at *,
  cases hxy with f hf,
  have h1 : tiene_inversa f := aux1 hf,
  cases h1 with g hg,
  use g,
  exact aux2 hf hg,
end

-- 2ª demostración
example : symmetric (⋍) :=
begin
  intros x y hxy,
  cases hxy with f hf,
  cases (aux1 hf) with g hg,
  use [g, aux2 hf hg],
end

-- 3ª demostración
example : symmetric (⋍) :=
begin
  rintros x y ⟨f, hf⟩,
  cases (aux1 hf) with g hg,
  use [g, aux2 hf hg],
end

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

variables {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)

def tiene_inversa (f : X → Y) :=

∃ g, inversa g f

lemma aux1

(hf : bijective f)

: tiene_inversa f :=

begin

cases (bijective_iff_has_inverse.mp hf) with g hg,

by tidy,

end

lemma aux2

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

bijective_iff_has_inverse.mpr (by use [f, hg])

-- 1ª demostración

example : symmetric (⋍) :=

begin

unfold symmetric,

intros x y hxy,

unfold es_equipotente at *,

cases hxy with f hf,

have h1 : tiene_inversa f := aux1 hf,

cases h1 with g hg,

use g,

exact aux2 hf hg,

end

-- 2ª demostración

example : symmetric (⋍) :=

begin

intros x y hxy,

cases hxy with f hf,

cases (aux1 hf) with g hg,

use [g, aux2 hf hg],

end

-- 3ª demostración

example : symmetric (⋍) :=

begin

rintros x y ⟨f, hf⟩,

cases (aux1 hf) with g hg,

use [g, aux2 hf hg],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La inversa de una función biyectiva es biyectiva

PorJosé A. Alonso 12 agosto 20215 agosto 2021

En Lean 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)

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

Demostrar que si la función f es biyectiva y g es una inversa de f, entonces g es biyectiva.

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

import tactic
open function

variables {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
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
sorry

import tactic

open function

variables {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

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

variables {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
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
begin
  rcases hg with ⟨h1, h2⟩,
  rw bijective_iff_has_inverse,
  use f,
  split,
  { exact h1, },
  { exact h2, },
end

-- 2ª demostración
example
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
begin
  rcases hg with ⟨h1, h2⟩,
  rw bijective_iff_has_inverse,
  use f,
  exact ⟨h1, h2⟩,
end

-- 3ª demostración
example
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
begin
  rcases hg with ⟨h1, h2⟩,
  rw bijective_iff_has_inverse,
  use [f, ⟨h1, h2⟩],
end

-- 4ª demostración
example
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
begin
  rw bijective_iff_has_inverse,
  use f,
  exact hg,
end

-- 5ª demostración
example
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
begin
  rw bijective_iff_has_inverse,
  use [f, hg],
end

-- 6ª demostración
example
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
begin
  apply bijective_iff_has_inverse.mpr,
  use [f, hg],
end

-- 7ª demostración
example
  (hf : bijective f)
  (hg : inversa g f)
  : bijective g :=
bijective_iff_has_inverse.mpr (by use [f, hg])

import tactic

open function

variables {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

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

begin

rcases hg with ⟨h1, h2⟩,

rw bijective_iff_has_inverse,

use f,

split,

{ exact h1, },

{ exact h2, },

end

-- 2ª demostración

example

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

begin

rcases hg with ⟨h1, h2⟩,

rw bijective_iff_has_inverse,

use f,

exact ⟨h1, h2⟩,

end

-- 3ª demostración

example

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

begin

rcases hg with ⟨h1, h2⟩,

rw bijective_iff_has_inverse,

use [f, ⟨h1, h2⟩],

end

-- 4ª demostración

example

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

begin

rw bijective_iff_has_inverse,

use f,

exact hg,

end

-- 5ª demostración

example

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

begin

rw bijective_iff_has_inverse,

use [f, hg],

end

-- 6ª demostración

example

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

begin

apply bijective_iff_has_inverse.mpr,

use [f, hg],

end

-- 7ª demostración

example

(hf : bijective f)

(hg : inversa g f)

: bijective g :=

bijective_iff_has_inverse.mpr (by use [f, hg])

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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 "bij f"
          "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(2) 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(2) 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 "bij f"
          "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(2) 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(2) inversa_def)
    then show "g (f x) = x" 
      by (simp only: o_apply)
  qed 
qed

end

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 "bij f"

"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(2) 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

show "surj g"

proof (rule surjI)

fix x

have h2 : "∀ x. (g ∘ f) x = x"

by (meson assms(2) inversa_def)

then have "(g ∘ f) x = x"

by (simp only: allE)

then show "g (f x) = x"

by (simp only: o_apply)

qed

(* 2ª demostración *)

lemma

fixes f :: "'a ⇒ 'b"

assumes "bij f"

"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(2) inversa_def)

then show "x = y"

by (metis ‹g x = g y› o_apply)

qed

show "surj g"

proof (rule surjI)

fix x

have h2 : "∀ x. (g ∘ f) x = x"

by (meson assms(2) inversa_def)

then show "g (f x) = x"

by (simp only: o_apply)

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

La equipotencia es una relación reflexiva

PorJosé A. Alonso 11 agosto 20215 agosto 2021

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*) :=
     ∃ g : A → B, bijective g

   infix ` ⋍ `: 50 := es_equipotente

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

Demostrar que la relación de equipotencia es reflexiva.

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

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g
infix ` ⋍ `: 50 := es_equipotente

example : reflexive (⋍) :=
sorry

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

example : reflexive (⋍) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

def es_equipotente (A B : Type*) :=
  ∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

-- 1ª demostración
example : reflexive (⋍) :=
begin
  intro X,
  use id,
  exact bijective_id,
end

-- 2ª demostración
example : reflexive (⋍) :=
begin
  intro X,
  use [id, bijective_id],
end

-- 3ª demostración
example : reflexive (⋍) :=
λ X, ⟨id, bijective_id⟩

-- 4ª demostración
example : reflexive (⋍) :=
by tidy

import tactic

open function

def es_equipotente (A B : Type*) :=

∃ g : A → B, bijective g

infix ` ⋍ `: 50 := es_equipotente

-- 1ª demostración

example : reflexive (⋍) :=

begin

intro X,

use id,

exact bijective_id,

end

-- 2ª demostración

example : reflexive (⋍) :=

begin

intro X,

use [id, bijective_id],

end

-- 3ª demostración

example : reflexive (⋍) :=

λ X, ⟨id, bijective_id⟩

-- 4ª demostración

example : reflexive (⋍) :=

by tidy

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Una función tiene inversa si y solo si es biyectiva

PorJosé A. Alonso 10 agosto 20215 agosto 2021

En Lean 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)

1 2	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 g f

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

Demostrar que la función f tiene inversa si y solo si f es biyectiva.

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

import tactic
open function

variables {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 : tiene_inversa f ↔ bijective f :=
sorry

import tactic

open function

variables {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 : tiene_inversa f ↔ bijective f :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

variables {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 : tiene_inversa f ↔ bijective f :=
begin
  split,
  { rintro ⟨g, ⟨h1, h2⟩⟩,
    split,
    { intros p q hf,
      calc p = g (f p) : (h2 p).symm
         ... = g (f q) : congr_arg g hf
         ... = q       : h2 q, },
    { intro y,
      use g y,
      exact h1 y, }},
  { rintro ⟨hfinj, hfsur⟩,
    choose g hg using hfsur,
    use g,
    split,
    { exact hg, },
    { intro a,
      apply hfinj,
      rw hg (f a), }},
end

-- 2ª demostración
example : tiene_inversa f ↔ bijective f :=
begin
  split,
  { rintro ⟨g, ⟨h1, h2⟩⟩,
    split,
    { intros p q hf,
      calc p = g (f p) : (h2 p).symm
         ... = g (f q) : congr_arg g hf
         ... = q       : h2 q, },
    { intro y,
      use [g y, h1 y], }},
  { rintro ⟨hfinj, hfsur⟩,
    choose g hg using hfsur,
    use g,
    split,
    { exact hg, },
    { intro a,
      exact @hfinj (g (f a)) a (hg (f a)), }},
end

-- 3ª demostración
example : tiene_inversa f ↔ bijective f :=
begin
  split,
  { rintro ⟨g, ⟨h1, h2⟩⟩,
    split,
    { intros p q hf,
      calc p = g (f p) : (h2 p).symm
         ... = g (f q) : congr_arg g hf
         ... = q       : h2 q, },
    { intro y,
      use [g y, h1 y], }},
  { rintro ⟨hfinj, hfsur⟩,
    choose g hg using hfsur,
    use g,
    exact ⟨hg, λ a, @hfinj (g (f a)) a (hg (f a))⟩, },
end

-- 4ª demostración
example
  : tiene_inversa f ↔ bijective f :=
begin
  split,
  { rintro ⟨g, ⟨h1, h2⟩⟩,
    split,
    { intros p q hf,
      calc p = g (f p) : (h2 p).symm
         ... = g (f q) : congr_arg g hf
         ... = q       : h2 q, },
    { intro y,
      use [g y, h1 y], }},
  { rintro ⟨hfinj, hfsur⟩,
    choose g hg using hfsur,
    use [g, ⟨hg, λ a, @hfinj (g (f a)) a (hg (f a))⟩], },
end

import tactic

open function

variables {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 : tiene_inversa f ↔ bijective f :=

begin

split,

{ rintro ⟨g, ⟨h1, h2⟩⟩,

split,

{ intros p q hf,

calc p = g (f p) : (h2 p).symm

... = g (f q) : congr_arg g hf

... = q : h2 q, },

{ intro y,

use g y,

exact h1 y, }},

{ rintro ⟨hfinj, hfsur⟩,

choose g hg using hfsur,

use g,

split,

{ exact hg, },

{ intro a,

apply hfinj,

rw hg (f a), }},

end

-- 2ª demostración

example : tiene_inversa f ↔ bijective f :=

begin

split,

{ rintro ⟨g, ⟨h1, h2⟩⟩,

split,

{ intros p q hf,

calc p = g (f p) : (h2 p).symm

... = g (f q) : congr_arg g hf

... = q : h2 q, },

{ intro y,

use [g y, h1 y], }},

{ rintro ⟨hfinj, hfsur⟩,

choose g hg using hfsur,

use g,

split,

{ exact hg, },

{ intro a,

exact @hfinj (g (f a)) a (hg (f a)), }},

end

-- 3ª demostración

example : tiene_inversa f ↔ bijective f :=

begin

split,

{ rintro ⟨g, ⟨h1, h2⟩⟩,

split,

{ intros p q hf,

calc p = g (f p) : (h2 p).symm

... = g (f q) : congr_arg g hf

... = q : h2 q, },

{ intro y,

use [g y, h1 y], }},

{ rintro ⟨hfinj, hfsur⟩,

choose g hg using hfsur,

use g,

exact ⟨hg, λ a, @hfinj (g (f a)) a (hg (f a))⟩, },

end

-- 4ª demostración

example

: tiene_inversa f ↔ bijective f :=

begin

split,

{ rintro ⟨g, ⟨h1, h2⟩⟩,

split,

{ intros p q hf,

calc p = g (f p) : (h2 p).symm

... = g (f q) : congr_arg g hf

... = q : h2 q, },

{ intro y,

use [g y, h1 y], }},

{ rintro ⟨hfinj, hfsur⟩,

choose g hg using hfsur,

use [g, ⟨hg, λ a, @hfinj (g (f a)) a (hg (f a))⟩], },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Una_funcion_tiene_inversa_si_y_solo_si_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)"

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

(* 1ª demostración *)
lemma "tiene_inversa f ⟷ bij f"
proof (rule iffI)
  assume "tiene_inversa f"
  then obtain g where h1 : "∀ x. (g ∘ f) x = x" and
                      h2 : "∀ y. (f ∘ g) y = y"
    using inversa_def tiene_inversa_def by metis
  show "bij f"
  proof (rule bijI)
    show "inj f"
    proof (rule injI)
      fix x y
      assume "f x = f y"
      then have "g (f x) = g (f y)"
        by simp
      then show "x = y"
        using h1 by simp
    qed
  next
    show "surj f"
    proof (rule surjI)
      fix y
      show "f (g y) = y"
        using h2 by simp
    qed
  qed
next
  assume "bij f"
  then have "surj f"
    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

(* 2ª demostración *)
lemma "tiene_inversa f ⟷ bij f"
proof (rule iffI)
  assume "tiene_inversa f"
  then obtain g where h1 : "∀ x. (g ∘ f) x = x" and
                      h2 : "∀ y. (f ∘ g) y = y"
    using inversa_def tiene_inversa_def by metis
  show "bij f"
  proof (rule bijI)
    show "inj f"
    proof (rule injI)
      fix x y
      assume "f x = f y"
      then have "g (f x) = g (f y)"
        by simp
      then show "x = y"
        using h1 by simp
    qed
  next
    show "surj f"
    proof (rule surjI)
      fix y
      show "f (g y) = y"
        using h2 by simp
    qed
  qed
next
  assume "bij f"
  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

100

101

102

103

104

105

106

107

108

theory Una_funcion_tiene_inversa_si_y_solo_si_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)"

definition tiene_inversa :: "('a ⇒ 'b) ⇒ bool" where

"tiene_inversa f ⟷ (∃ g. inversa f g)"

(* 1ª demostración *)

lemma "tiene_inversa f ⟷ bij f"

proof (rule iffI)

assume "tiene_inversa f"

then obtain g where h1 : "∀ x. (g ∘ f) x = x" and

h2 : "∀ y. (f ∘ g) y = y"

using inversa_def tiene_inversa_def by metis

show "bij f"

proof (rule bijI)

show "inj f"

proof (rule injI)

fix x y

assume "f x = f y"

then have "g (f x) = g (f y)"

by simp

then show "x = y"

using h1 by simp

qed

show "surj f"

proof (rule surjI)

fix y

show "f (g y) = y"

using h2 by simp

qed

assume "bij f"

then have "surj f"

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

show "∀y. (f ∘ g) y = y"

by (simp add: hg)

qed

then show "tiene_inversa f"

using tiene_inversa_def by auto

qed

(* 2ª demostración *)

lemma "tiene_inversa f ⟷ bij f"

proof (rule iffI)

assume "tiene_inversa f"

then obtain g where h1 : "∀ x. (g ∘ f) x = x" and

h2 : "∀ y. (f ∘ g) y = y"

using inversa_def tiene_inversa_def by metis

show "bij f"

proof (rule bijI)

show "inj f"

proof (rule injI)

fix x y

assume "f x = f y"

then have "g (f x) = g (f y)"

by simp

then show "x = y"

using h1 by simp

qed

show "surj f"

proof (rule surjI)

fix y

show "f (g y) = y"

using h2 by simp

qed

assume "bij f"

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)

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]