La inversa de una función es biyectiva
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 con Lean4 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} \newline &(∀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} \newline &(∀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