La_inversa_de_una_funcion_biyectiva_es_biyectiva.md

Título	Autor
La inversa de una función biyectiva es biyectiva	José A. Alonso

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)

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

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

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

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]