agosto 2021 – Página 2

Las sucesiones convergentes son sucesiones de Cauchy

PorJosé A. Alonso 21 agosto 202121 agosto 2021

Nota: El problema de hoy lo ha escrito Sara Díaz Real y es uno de los que se encuentran en su Trabajo Fin de Máster Formalización en Lean de problemas de las Olimpiadas Internacionales de Matemáticas (IMO). Concretamente, el problema se encuentra en la página 52 junto con la demostración en lenguaje natural.

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

Se define

el valor absoluto de x por

     notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

a es un límite de la sucesión u, por

     def limite (u : ℕ → ℝ) (a : ℝ) :=
       ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| ≤ ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, \|u n - a\| ≤ ε

la sucesión u es convergente por

     def suc_convergente (u : ℕ → ℝ) :=
       ∃ l, limite u l

1 2	def suc_convergente (u : ℕ → ℝ) := ∃ l, limite u l

la sucesión u es de Cauchy por

     def suc_cauchy (u : ℕ → ℝ) :=
       ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

1 2	def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, \|u p - u q\| ≤ ε

Demostrar que las sucesiones convergentes son de Cauchy.

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

import data.real.basic

variable {u : ℕ → ℝ }

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

def suc_convergente (u : ℕ → ℝ) :=
  ∃ l, limite u l

def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

example
  (h : suc_convergente u)
  : suc_cauchy u :=
sorry

import data.real.basic

variable {u : ℕ → ℝ }

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

def suc_convergente (u : ℕ → ℝ) :=

∃ l, limite u l

def suc_cauchy (u : ℕ → ℝ) :=

∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

example

(h : suc_convergente u)

: suc_cauchy u :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable {u : ℕ → ℝ }

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

def suc_convergente (u : ℕ → ℝ) :=
  ∃ l, limite u l

def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

-- 1ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  unfold suc_cauchy,
  intros ε hε,
  have hε2 : 0 < ε/2 := half_pos hε,
  cases h with l hl,
  cases hl (ε/2) hε2 with N hN,
  clear hε hl hε2,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : congr_arg2 (+) rfl (abs_sub_comm l (u q))
   ... ≤ ε/2 + ε/2               : add_le_add (hN p hp) (hN q hq)
   ... = ε                       : add_halves ε,
end

-- 2ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (half_pos hε) with N hN,
  clear hε hl,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : congr_arg2 (+) rfl (abs_sub_comm l (u q))
   ... ≤ ε/2 + ε/2               : add_le_add (hN p hp) (hN q hq)
   ... = ε                       : add_halves ε,
end

-- 3ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (half_pos hε) with N hN,
  clear hε hl,
  use N,
  intros p hp q hq,
  have cota1 : |u p - l| ≤ ε / 2 := hN p hp,
  have cota2 : |u q - l| ≤ ε / 2 := hN q hq,
  clear hN hp hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : by rw abs_sub_comm l (u q)
   ... ≤ ε                       : by linarith,
end

-- 4ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (half_pos hε) with N hN,
  clear hε hl,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : abs_add (u p - l) (l - u q)
   ... = |u p - l|  + |u q - l|  : by rw abs_sub_comm l (u q)
   ... ≤ ε                       : by linarith [hN p hp, hN q hq],
end

-- 5ª demostración
example
  (h : suc_convergente u)
  : suc_cauchy u :=
begin
  intros ε hε,
  cases h with l hl,
  cases hl (ε/2) (by linarith) with N hN,
  use N,
  intros p hp q hq,
  calc |u p - u q|
       = |(u p - l) + (l - u q)| : by ring_nf
   ... ≤ |u p - l|  + |l - u q|  : by simp [abs_add]
   ... = |u p - l|  + |u q - l|  : by simp [abs_sub_comm]
   ... ≤ ε                       : by linarith [hN p hp, hN q hq],
end

100

101

102

103

104

105

106

107

108

109

110

import data.real.basic

variable {u : ℕ → ℝ }

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (l : ℝ) : Prop :=

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

def suc_convergente (u : ℕ → ℝ) :=

∃ l, limite u l

def suc_cauchy (u : ℕ → ℝ) :=

∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε

-- 1ª demostración

example

(h : suc_convergente u)

: suc_cauchy u :=

begin

unfold suc_cauchy,

intros ε hε,

have hε2 : 0 < ε/2 := half_pos hε,

cases h with l hl,

cases hl (ε/2) hε2 with N hN,

clear hε hl hε2,

use N,

intros p hp q hq,

calc |u p - u q|

= |(u p - l) + (l - u q)| : by ring_nf

... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q)

... = |u p - l| + |u q - l| : congr_arg2 (+) rfl (abs_sub_comm l (u q))

... ≤ ε/2 + ε/2 : add_le_add (hN p hp) (hN q hq)

... = ε : add_halves ε,

end

-- 2ª demostración

example

(h : suc_convergente u)

: suc_cauchy u :=

begin

intros ε hε,

cases h with l hl,

cases hl (ε/2) (half_pos hε) with N hN,

clear hε hl,

use N,

intros p hp q hq,

calc |u p - u q|

= |(u p - l) + (l - u q)| : by ring_nf

... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q)

... = |u p - l| + |u q - l| : congr_arg2 (+) rfl (abs_sub_comm l (u q))

... ≤ ε/2 + ε/2 : add_le_add (hN p hp) (hN q hq)

... = ε : add_halves ε,

end

-- 3ª demostración

example

(h : suc_convergente u)

: suc_cauchy u :=

begin

intros ε hε,

cases h with l hl,

cases hl (ε/2) (half_pos hε) with N hN,

clear hε hl,

use N,

intros p hp q hq,

have cota1 : |u p - l| ≤ ε / 2 := hN p hp,

have cota2 : |u q - l| ≤ ε / 2 := hN q hq,

clear hN hp hq,

calc |u p - u q|

= |(u p - l) + (l - u q)| : by ring_nf

... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q)

... = |u p - l| + |u q - l| : by rw abs_sub_comm l (u q)

... ≤ ε : by linarith,

end

-- 4ª demostración

example

(h : suc_convergente u)

: suc_cauchy u :=

begin

intros ε hε,

cases h with l hl,

cases hl (ε/2) (half_pos hε) with N hN,

clear hε hl,

use N,

intros p hp q hq,

calc |u p - u q|

= |(u p - l) + (l - u q)| : by ring_nf

... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q)

... = |u p - l| + |u q - l| : by rw abs_sub_comm l (u q)

... ≤ ε : by linarith [hN p hp, hN q hq],

end

-- 5ª demostración

example

(h : suc_convergente u)

: suc_cauchy u :=

begin

intros ε hε,

cases h with l hl,

cases hl (ε/2) (by linarith) with N hN,

use N,

intros p hp q hq,

calc |u p - u q|

= |(u p - l) + (l - u q)| : by ring_nf

... ≤ |u p - l| + |l - u q| : by simp [abs_add]

... = |u p - l| + |u q - l| : by simp [abs_sub_comm]

... ≤ ε : by linarith [hN p hp, hN q hq],

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 Las_sucesiones_convergentes_son_sucesiones_de_Cauchy
imports Main HOL.Real
begin

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

definition suc_convergente :: "(nat ⇒ real) ⇒ bool"
  where "suc_convergente u ⟷ (∃ l. limite u l)"

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

(* 1ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
  proof (intro allI impI)
    fix p q
    assume hp : "p ≥ k" and hq : "q ≥ k"
    then have hp' : "¦u p - a¦ < ε/2"
      using hk by blast
    have hq' : "¦u q - a¦ < ε/2"
      using hk hq by blast
    have "¦u p - u q¦ = ¦(u p - a) + (a - u q)¦"
      by simp
    also have "… ≤ ¦u p - a¦  + ¦a - u q¦"
      by simp
    also have "… = ¦u p - a¦  + ¦u q - a¦"
      by simp
    also have "… < ε/2 + ε/2"
      using hp' hq' by simp
    also have "… = ε"
      by simp
    finally show "¦u p - u q¦ < ε"
      by this
  qed
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (rule exI)
qed

(* 2ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
  proof (intro allI impI)
    fix p q
    assume hp : "p ≥ k" and hq : "q ≥ k"
    then have hp' : "¦u p - a¦ < ε/2"
      using hk by blast
    have hq' : "¦u q - a¦ < ε/2"
      using hk hq by blast
    show "¦u p - u q¦ < ε"
      using hp' hq' by argo
  qed
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (rule exI)
qed

(* 3ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    using hk by (smt (z3) field_sum_of_halves)
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (rule exI)
qed

(* 3ª demostración *)
lemma
  assumes "suc_convergente u"
  shows   "suc_cauchy u"
proof (unfold suc_cauchy_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then have "0 < ε/2"
    by simp
  obtain a where "limite u a"
    using assms suc_convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"
    using ‹0 < ε / 2› limite_def by blast
  then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"
    by (smt (z3) field_sum_of_halves)
qed

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

theory Las_sucesiones_convergentes_son_sucesiones_de_Cauchy

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

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

definition suc_convergente :: "(nat ⇒ real) ⇒ bool"

where "suc_convergente u ⟷ (∃ l. limite u l)"

definition suc_cauchy :: "(nat ⇒ real) ⇒ bool"

where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"

(* 1ª demostración *)

lemma

assumes "suc_convergente u"

shows "suc_cauchy u"

proof (unfold suc_cauchy_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2"

by simp

obtain a where "limite u a"

using assms suc_convergente_def by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"

using ‹0 < ε / 2› limite_def by blast

have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

proof (intro allI impI)

fix p q

assume hp : "p ≥ k" and hq : "q ≥ k"

then have hp' : "¦u p - a¦ < ε/2"

using hk by blast

have hq' : "¦u q - a¦ < ε/2"

using hk hq by blast

have "¦u p - u q¦ = ¦(u p - a) + (a - u q)¦"

by simp

also have "… ≤ ¦u p - a¦ + ¦a - u q¦"

by simp

also have "… = ¦u p - a¦ + ¦u q - a¦"

by simp

also have "… < ε/2 + ε/2"

using hp' hq' by simp

also have "… = ε"

by simp

finally show "¦u p - u q¦ < ε"

by this

qed

then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "suc_convergente u"

shows "suc_cauchy u"

proof (unfold suc_cauchy_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2"

by simp

obtain a where "limite u a"

using assms suc_convergente_def by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"

using ‹0 < ε / 2› limite_def by blast

have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

proof (intro allI impI)

fix p q

assume hp : "p ≥ k" and hq : "q ≥ k"

then have hp' : "¦u p - a¦ < ε/2"

using hk by blast

have hq' : "¦u q - a¦ < ε/2"

using hk hq by blast

show "¦u p - u q¦ < ε"

using hp' hq' by argo

qed

then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

by (rule exI)

qed

(* 3ª demostración *)

lemma

assumes "suc_convergente u"

shows "suc_cauchy u"

proof (unfold suc_cauchy_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2"

by simp

obtain a where "limite u a"

using assms suc_convergente_def by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"

using ‹0 < ε / 2› limite_def by blast

have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

using hk by (smt (z3) field_sum_of_halves)

then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

by (rule exI)

qed

(* 3ª demostración *)

lemma

assumes "suc_convergente u"

shows "suc_cauchy u"

proof (unfold suc_cauchy_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2"

by simp

obtain a where "limite u a"

using assms suc_convergente_def by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2"

using ‹0 < ε / 2› limite_def by blast

then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε"

by (smt (z3) field_sum_of_halves)

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 composición por la izquierda con una inyectiva es una operación inyectiva

PorJosé A. Alonso 20 agosto 202121 agosto 2021

Sean f₁ y f₂ funciones de X en Y y g una función de X en Y. Demostrar que si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂.

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

import tactic

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

example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
sorry

import tactic

variables {X Y Z : Type*}

variables {f₁ f₂ : X → Y}

variable {g : Y → Z}

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

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

-- 1ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  calc g (f₁ x)
       = (g ∘ f₁) x : rfl
   ... = (g ∘ f₂) x : congr_fun hgf x
   ... = g (f₂ x)   : rfl,
end

-- 2ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  funext,
  apply hg,
  exact congr_fun hgf x,
end

-- 3ª demostración
example
  (hg : function.injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
begin
  refine funext (λ i, hg _),
  exact congr_fun hgf i,
end

-- 4ª demostración
example
  (hg : function.injective g)
  : function.injective ((∘) g : (X → Y) → (X → Z)) :=
λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))

-- 5ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : (left_id f₁).symm
    ... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl
    ... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _
    ... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf
    ... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _
    ... = id ∘ f₂              : congr_arg2 (∘) (inv_fun_comp hg) rfl
    ... = f₂                   : left_id f₂

-- 6ª demostración
example
  [hY : nonempty Y]
  (hg : injective g)
  (hgf : g ∘ f₁ = g ∘ f₂)
  : f₁ = f₂ :=
calc f₁ = id ∘ f₁              : by finish
    ... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]
    ... = inv_fun g ∘ (g ∘ f₁) : by refl
    ... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]
    ... = (inv_fun g ∘ g) ∘ f₂ : by refl
    ... = id ∘ f₂              : by finish [inv_fun_comp]
    ... = f₂                   : by finish

import tactic

variables {X Y Z : Type*}

variables {f₁ f₂ : X → Y}

variable {g : Y → Z}

-- 1ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

funext,

apply hg,

calc g (f₁ x)

= (g ∘ f₁) x : rfl

... = (g ∘ f₂) x : congr_fun hgf x

... = g (f₂ x) : rfl,

end

-- 2ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

funext,

apply hg,

exact congr_fun hgf x,

end

-- 3ª demostración

example

(hg : function.injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

begin

refine funext (λ i, hg _),

exact congr_fun hgf i,

end

-- 4ª demostración

example

(hg : function.injective g)

: function.injective ((∘) g : (X → Y) → (X → Z)) :=

λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))

-- 5ª demostración

example

[hY : nonempty Y]

(hg : injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

calc f₁ = id ∘ f₁ : (left_id f₁).symm

... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl

... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _

... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf

... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _

... = id ∘ f₂ : congr_arg2 (∘) (inv_fun_comp hg) rfl

... = f₂ : left_id f₂

-- 6ª demostración

example

[hY : nonempty Y]

(hg : injective g)

(hgf : g ∘ f₁ = g ∘ f₂)

: f₁ = f₂ :=

calc f₁ = id ∘ f₁ : by finish

... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp]

... = inv_fun g ∘ (g ∘ f₁) : by refl

... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf]

... = (inv_fun g ∘ g) ∘ f₂ : by refl

... = id ∘ f₂ : by finish [inv_fun_comp]

... = f₂ : by finish

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_por_la_izquierda_con_una_inyectiva_es_inyectiva
imports Main
begin

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

(* 2ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof
  fix x
  have "(g ∘ f1) x = (g ∘ f2) x"
    using ‹g ∘ f1 = g ∘ f2› by simp
  then have "g (f1 x) = g (f2 x)"
    by simp
  then show "f1 x = f2 x"
    using ‹inj g› by (simp only: injD)
qed

(* 3ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
using assms
by (metis fun.inj_map_strong inj_eq)

(* 4ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = id ∘ f1"
    by (rule id_o [symmetric])
  also have "… = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = inv g ∘ (g ∘ f1)"
    by (simp add: comp_assoc)
  also have "… = inv g ∘ (g ∘ f2)"
    using assms(2) by (rule arg_cong)
  also have "… = (inv g ∘ g) ∘ f2"
    by (simp add: comp_assoc)
  also have "… = id ∘ f2"
    by (simp add: assms(1))
  also have "… = f2"
    by (rule id_o)
  finally show "f1 = f2"
    by this
qed

(* 5ª demostración *)
lemma
  assumes "inj g"
          "g ∘ f1 = g ∘ f2"
  shows   "f1 = f2"
proof -
  have "f1 = (inv g ∘ g) ∘ f1"
    by (simp add: assms(1))
  also have "… = (inv g ∘ g) ∘ f2"
    using assms(2) by (simp add: comp_assoc)
  also have "… = f2"
    using assms(1) by simp
  finally show "f1 = f2" .
qed

end

theory La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva

imports Main

begin

(* 1ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof (rule ext)

fix x

have "(g ∘ f1) x = (g ∘ f2) x"

using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong)

then have "g (f1 x) = g (f2 x)"

by (simp only: o_apply)

then show "f1 x = f2 x"

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

qed

(* 2ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof

fix x

have "(g ∘ f1) x = (g ∘ f2) x"

using ‹g ∘ f1 = g ∘ f2› by simp

then have "g (f1 x) = g (f2 x)"

by simp

then show "f1 x = f2 x"

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

qed

(* 3ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

using assms

by (metis fun.inj_map_strong inj_eq)

(* 4ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof -

have "f1 = id ∘ f1"

by (rule id_o [symmetric])

also have "… = (inv g ∘ g) ∘ f1"

by (simp add: assms(1))

also have "… = inv g ∘ (g ∘ f1)"

by (simp add: comp_assoc)

also have "… = inv g ∘ (g ∘ f2)"

using assms(2) by (rule arg_cong)

also have "… = (inv g ∘ g) ∘ f2"

by (simp add: comp_assoc)

also have "… = id ∘ f2"

by (simp add: assms(1))

also have "… = f2"

by (rule id_o)

finally show "f1 = f2"

by this

qed

(* 5ª demostración *)

lemma

assumes "inj g"

"g ∘ f1 = g ∘ f2"

shows "f1 = f2"

proof -

have "f1 = (inv g ∘ g) ∘ f1"

by (simp add: assms(1))

also have "… = (inv g ∘ g) ∘ f2"

using assms(2) by (simp add: comp_assoc)

also have "… = f2"

using assms(1) by simp

finally show "f1 = f2" .

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