Skip to content

Latest commit

 

History

History
239 lines (200 loc) · 5.44 KB

La_inversa_de_una_funcion_biyectiva_es_biyectiva.md

File metadata and controls

239 lines (200 loc) · 5.44 KB
title date category has_math
La inversa de una función es biyectiva
2024-06-19 06:00:00 UTC+02:00
Funciones
true

[mathjax]

En Lean4 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 \(g\) es una inversa de \(f\), entonces \(g\) es biyectiva.

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

import Mathlib.Tactic
open Function

variable {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
  (hg : inversa g f)
  : Bijective g :=
by sorry

1. Demostración en lenguaje natural

Para demostrar que \(g: Y → X\) es biyectiva, basta probar que existe una \(h\) que es inversa de \(g\) por la izquierda y por la derecha; es decir, \begin{align} &(∀y ∈ Y)[(h ∘ g)(y) = y] \tag{1} \\ &(∀x ∈ X)[(g ∘ h)(x) = x] \tag{2} \end{align}

Puesto que \(g\) es una inversa de \(f\), entonces \begin{align} &(∀x ∈ X)[(g ∘ f)(x) = x] \tag{3} \\ &(∀y ∈ Y)[(f ∘ g)(y) = y] \tag{4} \end{align}

Tomando \(f\) como \(h\), (1) se verifica por (4) y (2) se verifica por (3).

2. Demostraciones con Lean4

import Mathlib.Tactic
open Function

variable {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
  (hg : inversa g f)
  : Bijective g :=
by
  rcases hg with ⟨h1, h2⟩
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  use f
  -- ⊢ LeftInverse f g ∧ Function.RightInverse f g
  constructor
  . -- ⊢ LeftInverse f g
    exact h1
  . -- ⊢ Function.RightInverse f g
    exact h2

-- 2ª demostración
-- ===============

example
  (hg : inversa g f)
  : Bijective g :=
by
  rcases hg with ⟨h1, h2⟩
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  use f
  -- ⊢ LeftInverse f g ∧ Function.RightInverse f g
  exact ⟨h1, h2⟩

-- 3ª demostración
-- ===============

example
  (hg : inversa g f)
  : Bijective g :=
by
  rcases hg with ⟨h1, h2⟩
  -- h1 : ∀ (x : Y), (f ∘ g) x = x
  -- h2 : ∀ (y : X), (g ∘ f) y = y
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, ⟨h1, h2⟩⟩

-- 4ª demostración
-- ===============

example
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  use f
  -- ⊢ LeftInverse f g ∧ Function.RightInverse f g
  exact hg

-- 5ª demostración
-- ===============

example
  (hg : inversa g f)
  : Bijective g :=
by
  rw [bijective_iff_has_inverse]
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

-- 6ª demostración
-- ===============

example
  (hg : inversa g f)
  : Bijective g :=
by
  apply bijective_iff_has_inverse.mpr
  -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g
  exact ⟨f, hg⟩

-- Lemas usados
-- ============

-- #check (bijective_iff_has_inverse : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones 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 "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 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 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 "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 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 inversa_def)
    then show "g (f x) = x"
      by (simp only: o_apply)
  qed
qed

end