4 agosto 2021 – Calculemus

Una función tiene inversa por la izquierda si y solo si es inyectiva

PorJosé A. Alonso 4 agosto 20213 agosto 2021

En Lean, que g es una inversa por la izquierda de f está definido por

   left_inverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

1 2	left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x

y que f tenga inversa por la izquierda está definido por

   has_left_inverse (f : α → β) : Prop :=
      ∃ finv : β → α, left_inverse finv f

1 2	has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f

Finalmente, que f es inyectiva está definido por

   injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

1 2	injective (f : α → β) : Prop := ∀ ⦃x y⦄, f x = f y → x = y

Demostrar que una función f, con dominio no vacío, tiene inversa por la izquierda si y solo si es inyectiva.

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

import tactic
open function

variables {α : Type*} [nonempty α]
variable  {β : Type*}
variable  {f : α → β}

example :
  has_left_inverse f ↔ injective f :=
sorry

import tactic

open function

variables {α : Type*} [nonempty α]

variable {β : Type*}

variable {f : α → β}

example :

has_left_inverse f ↔ injective f :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

variables {α : Type*} [nonempty α]
variable  {β : Type*}
variable  {f : α → β}

-- 1ª demostración
example : has_left_inverse f ↔ injective f :=
begin
  split,
  { intro hf,
    intros x y hxy,
    cases hf with g hg,
    calc x = g (f x) : (hg x).symm
       ... = g (f y) : congr_arg g hxy
       ... = y       : hg y, },
  { intro hf,
    use inv_fun f,
    intro x,
    apply hf,
    apply inv_fun_eq,
    use x, },
end

-- 2ª demostración
example : has_left_inverse f ↔ injective f :=
begin
  split,
  { intro hf,
    exact has_left_inverse.injective hf },
  { intro hf,
    exact injective.has_left_inverse hf },
end

-- 3ª demostración
example : has_left_inverse f ↔ injective f :=
⟨has_left_inverse.injective, injective.has_left_inverse⟩

-- 4ª demostración
example : has_left_inverse f ↔ injective f :=
injective_iff_has_left_inverse.symm

import tactic

open function

variables {α : Type*} [nonempty α]

variable {β : Type*}

variable {f : α → β}

-- 1ª demostración

example : has_left_inverse f ↔ injective f :=

begin

split,

{ intro hf,

intros x y hxy,

cases hf with g hg,

calc x = g (f x) : (hg x).symm

... = g (f y) : congr_arg g hxy

... = y : hg y, },

{ intro hf,

use inv_fun f,

intro x,

apply hf,

apply inv_fun_eq,

use x, },

end

-- 2ª demostración

example : has_left_inverse f ↔ injective f :=

begin

split,

{ intro hf,

exact has_left_inverse.injective hf },

{ intro hf,

exact injective.has_left_inverse hf },

end

-- 3ª demostración

example : has_left_inverse f ↔ injective f :=

⟨has_left_inverse.injective, injective.has_left_inverse⟩

-- 4ª demostración

example : has_left_inverse f ↔ injective f :=

injective_iff_has_left_inverse.symm

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

definition tiene_inversa_izq :: "('a ⇒ 'b) ⇒ bool" where
  "tiene_inversa_izq f ⟷ (∃g. ∀x. g (f x) = x)"

(* 1ª demostración *)
lemma
  "tiene_inversa_izq f ⟷ inj f"
proof (rule iffI)
  assume "tiene_inversa_izq f"
  show "inj f"
  proof (unfold inj_def; intro allI impI)
    fix x y
    assume "f x = f y"
    obtain g where hg : "∀x. g (f x) = x"
      using ‹tiene_inversa_izq f› tiene_inversa_izq_def
      by auto
    have "x = g (f x)"
      by (simp only: hg)
    also have "… = g (f y)"
      by (simp only: ‹f x = f y›)
    also have "… = y"
      by (simp only: hg)
    finally show "x = y" .
  qed
next
  assume "inj f"
  show "tiene_inversa_izq f"
  proof (unfold tiene_inversa_izq_def)
    have "∀x. inv f (f x) = x"
    proof (rule allI)
      fix x
      show "inv f (f x) = x"
        using ‹inj f› by (simp only: inv_f_f)
    qed
  then show "(∃g. ∀x. g (f x) = x)"
    by (simp only: exI)
  qed
qed

(* 2ª demostración *)
lemma
  "tiene_inversa_izq f ⟷ inj f"
proof (rule iffI)
  assume "tiene_inversa_izq f"
  then show "inj f"
    by (metis inj_def tiene_inversa_izq_def)
next
  assume "inj f"
  then show "tiene_inversa_izq f"
    by (metis the_inv_f_f tiene_inversa_izq_def)
qed

(* 3ª demostración *)
lemma
  "tiene_inversa_izq f ⟷ inj f"
by (metis tiene_inversa_izq_def inj_def the_inv_f_f)

end

theory Una_funcion_tiene_inversa_por_la_izquierda_si_y_solo_si_es_inyectiva

imports Main

begin

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

"tiene_inversa_izq f ⟷ (∃g. ∀x. g (f x) = x)"

(* 1ª demostración *)

lemma

"tiene_inversa_izq f ⟷ inj f"

proof (rule iffI)

assume "tiene_inversa_izq f"

show "inj f"

proof (unfold inj_def; intro allI impI)

fix x y

assume "f x = f y"

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

using ‹tiene_inversa_izq f› tiene_inversa_izq_def

by auto

have "x = g (f x)"

by (simp only: hg)

also have "… = g (f y)"

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

also have "… = y"

by (simp only: hg)

finally show "x = y" .

qed

assume "inj f"

show "tiene_inversa_izq f"

proof (unfold tiene_inversa_izq_def)

have "∀x. inv f (f x) = x"

proof (rule allI)

fix x

show "inv f (f x) = x"

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

qed

then show "(∃g. ∀x. g (f x) = x)"

by (simp only: exI)

qed

(* 2ª demostración *)

lemma

"tiene_inversa_izq f ⟷ inj f"

proof (rule iffI)

assume "tiene_inversa_izq f"

then show "inj f"

by (metis inj_def tiene_inversa_izq_def)

assume "inj f"

then show "tiene_inversa_izq f"

by (metis the_inv_f_f tiene_inversa_izq_def)

qed

(* 3ª demostración *)

lemma

"tiene_inversa_izq f ⟷ inj f"

by (metis tiene_inversa_izq_def inj_def the_inv_f_f)

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]