Las funciones inyectivas tienen inversa por la izquierda
En Lean, que g es una inversa por la izquierda de f está definido por
|
1 2 |
left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x |
y que f tenga inversa por la izquierda está definido por
|
1 2 |
has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f |
Finalmente, que f es inyectiva está definido por
|
1 2 |
injective (f : α → β) : Prop := ∀ ⦃x y⦄, f x = f y → x = y |
Demostrar que si f es una función inyectiva con dominio no vacío, entonces f tiene inversa por la izquierda.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import tactic open function classical variables {α β: Type*} variable {f : α → β} -- 1ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse 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 79 80 81 82 83 |
import tactic open function classical variables {α β: Type*} variable {f : α → β} -- 1ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse f := begin classical, unfold has_left_inverse, let g := λ y, if h : ∃ x, f x = y then some h else choice hα, use g, unfold left_inverse, intro a, have h1 : ∃ x : α, f x = f a := Exists.intro a rfl, dsimp at *, dsimp [g], rw dif_pos h1, apply hf, exact some_spec h1, end -- 2ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse f := begin classical, let g := λ y, if h : ∃ x, f x = y then some h else choice hα, use g, intro a, have h1 : ∃ x : α, f x = f a := Exists.intro a rfl, dsimp [g], rw dif_pos h1, exact hf (some_spec h1), end -- 3ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse f := begin unfold has_left_inverse, use inv_fun f, unfold left_inverse, intro x, apply hf, apply inv_fun_eq, use x, end -- 4ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse f := begin use inv_fun f, intro x, apply hf, apply inv_fun_eq, use x, end -- 5ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse f := ⟨inv_fun f, left_inverse_inv_fun hf⟩ -- 6ª demostración example [hα : nonempty α] (hf : injective f) : has_left_inverse f := injective.has_left_inverse hf |
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 |
theory Las_funciones_inyectivas_tienen_inversa_por_la_izquierda imports Main begin definition tiene_inversa_izq :: "('a ⇒ 'b) ⇒ bool" where "tiene_inversa_izq f ⟷ (∃g. ∀x. g (f x) = x)" (* 1ª demostración *) lemma assumes "inj f" shows "tiene_inversa_izq f" proof (unfold tiene_inversa_izq_def) let ?g = "(λy. SOME x. f x = y)" have "∀x. ?g (f x) = x" proof (rule allI) fix a have "∃x. f x = f a" by auto then have "f (?g (f a)) = f a" by (rule someI_ex) then show "?g (f a) = a" using assms by (simp only: injD) qed then show "(∃g. ∀x. g (f x) = x)" by (simp only: exI) qed (* 2ª demostración *) lemma assumes "inj f" shows "tiene_inversa_izq f" proof (unfold tiene_inversa_izq_def) have "∀x. inv f (f x) = x" proof (rule allI) fix x show "inv f (f x) = x" using assms by (simp only: inv_f_f) qed then show "(∃g. ∀x. g (f x) = x)" by (simp only: exI) qed (* 3ª demostración *) lemma assumes "inj f" shows "tiene_inversa_izq f" proof (unfold tiene_inversa_izq_def) have "∀x. inv f (f x) = x" by (simp add: assms) then show "(∃g. ∀x. g (f x) = x)" by (simp only: exI) 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]
