Las funciones biyectivas tienen inversa
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) |
y que f tiene inversa por
1 2 |
def tiene_inversa (f : X → Y) := ∃ g, inversa g f |
Demostrar que si la función f es biyectiva, entonces f tiene inversa.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 |
import tactic open function variables {X Y : Type*} variable (f : X → Y) def inversa (f : X → Y) (g : Y → X) := (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y) def tiene_inversa (f : X → Y) := ∃ g, inversa g f example (hf : bijective f) : tiene_inversa f := 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 |
import tactic open function variables {X Y : Type*} variable (f : X → Y) def inversa (f : X → Y) (g : Y → X) := (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y) def tiene_inversa (f : X → Y) := ∃ g, inversa g f -- 1ª demostración example (hf : bijective f) : tiene_inversa f := begin rcases hf with ⟨hfiny, hfsup⟩, choose g hg using hfsup, use g, split, { exact hg, }, { intro a, apply hfiny, rw hg (f a), }, end -- 2ª demostración example (hf : bijective f) : tiene_inversa f := begin rcases hf with ⟨hfiny, hfsup⟩, choose g hg using hfsup, use g, split, { exact hg, }, { intro a, exact @hfiny (g (f a)) a (hg (f a)), }, end -- 3ª demostración example (hf : bijective f) : tiene_inversa f := begin rcases hf with ⟨hfiny, hfsup⟩, choose g hg using hfsup, use g, exact ⟨hg, λ a, @hfiny (g (f a)) a (hg (f a))⟩, end -- 4ª demostración example (hf : bijective f) : tiene_inversa f := begin rcases hf with ⟨hfiny, hfsup⟩, choose g hg using hfsup, use [g, ⟨hg, λ a, @hfiny (g (f a)) a (hg (f a))⟩], end -- 5ª demostración example (hf : bijective f) : tiene_inversa f := begin cases (bijective_iff_has_inverse.mp hf) with g hg, by tidy, end |
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 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 |
theory Las_funciones_biyectivas_tienen_inversa imports Main begin definition inversa :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ bool" where "inversa f g ⟷ (∀ x. (g ∘ f) x = x) ∧ (∀ y. (f ∘ g) y = y)" definition tiene_inversa :: "('a ⇒ 'b) ⇒ bool" where "tiene_inversa f ⟷ (∃ g. inversa f g)" (* 1ª demostración *) lemma assumes "bij f" shows "tiene_inversa f" proof - have "surj f" using assms by (rule bij_is_surj) then obtain g where hg : "∀y. f (g y) = y" by (metis surjD) have "inversa f g" proof (unfold inversa_def; intro conjI) show "∀x. (g ∘ f) x = x" proof (rule allI) fix x have "inj f" using ‹bij f› by (rule bij_is_inj) then show "(g ∘ f) x = x" proof (rule injD) have "f ((g ∘ f) x) = f (g (f x))" by simp also have "… = f x" by (simp add: hg) finally show "f ((g ∘ f) x) = f x" by this qed qed next show "∀y. (f ∘ g) y = y" by (simp add: hg) qed then show "tiene_inversa f" using tiene_inversa_def by blast qed (* 2ª demostración *) lemma assumes "bij f" shows "tiene_inversa f" proof - have "surj f" using assms by (rule bij_is_surj) then obtain g where hg : "∀y. f (g y) = y" by (metis surjD) have "inversa f g" proof (unfold inversa_def; intro conjI) show "∀x. (g ∘ f) x = x" proof (rule allI) fix x have "inj f" using ‹bij f› by (rule bij_is_inj) then show "(g ∘ f) x = x" proof (rule injD) have "f ((g ∘ f) x) = f (g (f x))" by simp also have "… = f x" by (simp add: hg) finally show "f ((g ∘ f) x) = f x" by this qed qed next show "∀y. (f ∘ g) y = y" by (simp add: hg) qed then show "tiene_inversa f" using tiene_inversa_def by auto qed (* 3ª demostración *) lemma assumes "bij f" shows "tiene_inversa f" proof - have "inversa f (inv f)" proof (unfold inversa_def; intro conjI) show "∀x. (inv f ∘ f) x = x" by (simp add: ‹bij f› bij_is_inj) next show "∀y. (f ∘ inv f) y = y" by (simp add: ‹bij f› bij_is_surj surj_f_inv_f) qed then show "tiene_inversa f" using tiene_inversa_def by auto 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]