Funciones – Página 3

f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]

PorJosé A. Alonso 12 marzo 20249 marzo 2024

En Lean, la imagen inversa de un conjunto s (de elementos de tipo β) por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.

Demostrar con Lean4 que

   f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v

1	f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v

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

import Mathlib.Data.Set.Function
variable {α β : Type _}
variable (f : α → β)
variable (u v : Set β)
open Set

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
by sorry

import Mathlib.Data.Set.Function

variable {α β : Type _}

variable (f : α → β)

variable (u v : Set β)

open Set

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

by sorry

Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales

PorJosé A. Alonso 30 enero 202417 febrero 2024

Demostrar con Lean4 que las funciones \(f(x,y) = (x + y)²\) y \(g(x,y) = x² + 2xy + y\)² son iguales.

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

import  Mathlib.Data.Real.Basic

example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) :=
by sorry

import Mathlib.Data.Real.Basic

example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) :=

by sorry

Imagen inversa de la intersección

PorJosé A. Alonso 30 abril 20221 mayo 2022

En Lean, la imagen inversa de un conjunto s (de elementos de tipo por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.

Demostrar que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v

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

import data.set.basic

open set

variables {α : Type*} {β : Type*}
variable  f : α → β
variables u v : set β

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=
sorry

import data.set.basic

open set

variables {α : Type*} {β : Type*}

variable f : α → β

variables u v : set β

example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v :=

sorry

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

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]

Las funciones biyectivas tienen inversa

PorJosé A. Alonso 9 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 si la función f es biyectiva, entonces f tiene inversa.

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
  (hf : bijective f)
  : tiene_inversa 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

(hf : bijective f)

: tiene_inversa 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
  (hf : bijective f)
  : tiene_inversa f :=
begin
  rcases hf with ⟨hfiny, hfsup⟩,
  choose g hg using hfsup,
  use g,
  split,
  { exact hg, },
  { intro a,
    apply hfiny,
    rw hg (f a), },
end

-- 2ª demostración
example
  (hf : bijective f)
  : tiene_inversa f :=
begin
  rcases hf with ⟨hfiny, hfsup⟩,
  choose g hg using hfsup,
  use g,
  split,
  { exact hg, },
  { intro a,
    exact @hfiny (g (f a)) a (hg (f a)), },
end

-- 3ª demostración
example
  (hf : bijective f)
  : tiene_inversa f :=
begin
  rcases hf with ⟨hfiny, hfsup⟩,
  choose g hg using hfsup,
  use g,
  exact ⟨hg, λ a, @hfiny (g (f a)) a (hg (f a))⟩,
end

-- 4ª demostración
example
  (hf : bijective f)
  : tiene_inversa f :=
begin
  rcases hf with ⟨hfiny, hfsup⟩,
  choose g hg using hfsup,
  use [g, ⟨hg, λ a, @hfiny (g (f a)) a (hg (f a))⟩],
end

-- 5ª demostración
example
  (hf : bijective f)
  : tiene_inversa f :=
begin
  cases (bijective_iff_has_inverse.mp hf) with g hg,
  by tidy,
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

(hf : bijective f)

: tiene_inversa f :=

begin

rcases hf with ⟨hfiny, hfsup⟩,

choose g hg using hfsup,

use g,

split,

{ exact hg, },

{ intro a,

apply hfiny,

rw hg (f a), },

end

-- 2ª demostración

example

(hf : bijective f)

: tiene_inversa f :=

begin

rcases hf with ⟨hfiny, hfsup⟩,

choose g hg using hfsup,

use g,

split,

{ exact hg, },

{ intro a,

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

end

-- 3ª demostración

example

(hf : bijective f)

: tiene_inversa f :=

begin

rcases hf with ⟨hfiny, hfsup⟩,

choose g hg using hfsup,

use g,

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

end

-- 4ª demostración

example

(hf : bijective f)

: tiene_inversa f :=

begin

rcases hf with ⟨hfiny, hfsup⟩,

choose g hg using hfsup,

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

end

-- 5ª demostración

example

(hf : bijective f)

: tiene_inversa f :=

begin

cases (bijective_iff_has_inverse.mp hf) with g hg,

by tidy,

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

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

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

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

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

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

end

theory Las_funciones_biyectivas_tienen_inversa

imports Main

begin

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

"inversa f g ⟷ (∀ x. (g ∘ f) x = x) ∧ (∀ y. (f ∘ g) y = y)"

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

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

(* 1ª demostración *)

lemma

assumes "bij f"

shows "tiene_inversa f"

proof -

have "surj f"

using assms by (rule bij_is_surj)

then obtain g where hg : "∀y. f (g y) = y"

by (metis surjD)

have "inversa f g"

proof (unfold inversa_def; intro conjI)

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

proof (rule allI)

fix x

have "inj f"

using ‹bij f› by (rule bij_is_inj)

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

proof (rule injD)

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

by simp

also have "… = f x"

by (simp add: hg)

finally show "f ((g ∘ f) x) = f x"

by this

qed

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

by (simp add: hg)

qed

then show "tiene_inversa f"

using tiene_inversa_def by blast

qed

(* 2ª demostración *)

lemma

assumes "bij f"

shows "tiene_inversa f"

proof -

have "surj f"

using assms by (rule bij_is_surj)

then obtain g where hg : "∀y. f (g y) = y"

by (metis surjD)

have "inversa f g"

proof (unfold inversa_def; intro conjI)

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

proof (rule allI)

fix x

have "inj f"

using ‹bij f› by (rule bij_is_inj)

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

proof (rule injD)

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

by simp

also have "… = f x"

by (simp add: hg)

finally show "f ((g ∘ f) x) = f x"

by this

qed

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

by (simp add: hg)

qed

then show "tiene_inversa f"

using tiene_inversa_def by auto

qed

(* 3ª demostración *)

lemma

assumes "bij f"

shows "tiene_inversa f"

proof -

have "inversa f (inv f)"

proof (unfold inversa_def; intro conjI)

show "∀x. (inv f ∘ f) x = x"

by (simp add: ‹bij f› bij_is_inj)

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]