2 agosto 2021 – Calculemus

Las funciones con inversa por la izquierda son inyectivas

PorJosé A. Alonso 2 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 si f tiene inversa por la izquierda, entonces f es inyectiva.

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

import tactic
open function

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


example
  (hf : has_left_inverse f)
  : injective f :=
sorry

import tactic

open function

universes u v

variables {α : Type u}

variable {β : Type v}

variable {f : α → β}

example

(hf : has_left_inverse f)

: injective f :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open function

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

-- 1ª demostración
example
  (hf : has_left_inverse f)
  : injective f :=
begin
  intros x y hxy,
  unfold has_left_inverse at hf,
  unfold left_inverse at hf,
  cases hf with g hg,
  calc x = g (f x) : (hg x).symm
     ... = g (f y) : congr_arg g hxy
     ... = y       : hg y
end

-- 2ª demostración
example
  (hf : has_left_inverse f)
  : injective f :=
begin
  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
end

-- 3ª demostración
example
  (hf : has_left_inverse f)
  : injective f :=
exists.elim hf (λ finv inv, inv.injective)

-- 4ª demostración
example
  (hf : has_left_inverse f)
  : injective f :=
has_left_inverse.injective hf

import tactic

open function

universes u v

variables {α : Type u}

variable {β : Type v}

variable {f : α → β}

-- 1ª demostración

example

(hf : has_left_inverse f)

: injective f :=

begin

intros x y hxy,

unfold has_left_inverse at hf,

unfold left_inverse at hf,

cases hf with g hg,

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

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

... = y : hg y

end

-- 2ª demostración

example

(hf : has_left_inverse f)

: injective f :=

begin

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

end

-- 3ª demostración

example

(hf : has_left_inverse f)

: injective f :=

exists.elim hf (λ finv inv, inv.injective)

-- 4ª demostración

example

(hf : has_left_inverse f)

: injective f :=

has_left_inverse.injective 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 Las_funciones_con_inversa_por_la_izquierda_son_inyectivas
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
  assumes "tiene_inversa_izq f"
  shows   "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 assms 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

(* 2ª demostración *)
lemma
  assumes "tiene_inversa_izq f"
  shows   "inj f"
  by (metis assms inj_def tiene_inversa_izq_def)

end

theory Las_funciones_con_inversa_por_la_izquierda_son_inyectivas

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

assumes "tiene_inversa_izq f"

shows "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 assms 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

(* 2ª demostración *)

lemma

assumes "tiene_inversa_izq f"

shows "inj f"

by (metis assms inj_def tiene_inversa_izq_def)

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]