La inversa de una función biyectiva es biyectiva
En Lean se puede definir que g es una inversa de f por
1 2 |
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:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
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»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 |
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»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 |
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]