Las funciones con inversa son biyectivas
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 tiene inversa, entonces f 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 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 : tiene_inversa f) : bijective 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 71 72 73 74 75 76 77 78 |
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 : tiene_inversa f) : bijective f := begin rcases hf with ⟨g, ⟨h1, h2⟩⟩, split, { intros a b hab, calc a = g (f a) : (h2 a).symm ... = g (f b) : congr_arg g hab ... = b : h2 b, }, { intro y, use g y, exact h1 y, }, end -- 2ª demostración example (hf : tiene_inversa f) : bijective f := begin rcases hf with ⟨g, ⟨h1, h2⟩⟩, split, { intros a b hab, calc a = g (f a) : (h2 a).symm ... = g (f b) : congr_arg g hab ... = b : h2 b, }, { intro y, use [g y, h1 y], }, end -- 3ª demostración example (hf : tiene_inversa f) : bijective f := begin rcases hf with ⟨g, ⟨h1, h2⟩⟩, split, { exact left_inverse.injective h2, }, { exact right_inverse.surjective h1, }, end -- 4ª demostración example (hf : tiene_inversa f) : bijective f := begin rcases hf with ⟨g, ⟨h1, h2⟩⟩, exact ⟨left_inverse.injective h2, right_inverse.surjective h1⟩, end -- 5ª demostración example : tiene_inversa f → bijective f := begin rintros ⟨g, ⟨h1, h2⟩⟩, exact ⟨left_inverse.injective h2, right_inverse.surjective h1⟩, end -- 6ª demostración example : tiene_inversa f → bijective f := λ ⟨g, ⟨h1, h2⟩⟩, ⟨left_inverse.injective h2, right_inverse.surjective h1⟩ |
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 |
theory Las_funciones_con_inversa_son_biyectivas 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 fixes f :: "'a ⇒ 'b" assumes "tiene_inversa f" shows "bij f" proof - obtain g where h1 : "∀ x. (g ∘ f) x = x" and h2 : "∀ y. (f ∘ g) y = y" by (meson assms inversa_def tiene_inversa_def) show "bij f" proof (rule bijI) show "inj f" proof (rule injI) fix x y assume "f x = f y" then have "g (f x) = g (f y)" by simp then show "x = y" using h1 by simp qed next show "surj f" proof (rule surjI) fix y show "f (g y) = y" using h2 by simp qed qed qed (* 2ª demostración *) lemma fixes f :: "'a ⇒ 'b" assumes "tiene_inversa f" shows "bij f" proof - obtain g where h1 : "∀ x. (g ∘ f) x = x" and h2 : "∀ y. (f ∘ g) y = y" by (meson assms inversa_def tiene_inversa_def) show "bij f" proof (rule bijI) show "inj f" proof (rule injI) fix x y assume "f x = f y" then have "g (f x) = g (f y)" by simp then show "x = y" using h1 by simp qed next show "surj f" proof (rule surjI) fix y show "f (g y) = y" using h2 by simp qed 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]