Las funciones con inversa por la derecha son suprayectivas
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 |
que g es una inversa por la derecha de f está definido por
1 2 |
right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g |
y que f tenga inversa por la derecha está definido por
1 2 |
has_right_inverse (f : α → β) : Prop := ∃ g : β → α, right_inverse g f |
Finalmente, que f es suprayectiva está definido por
1 2 |
def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b |
Demostrar que si la función f tiene inversa por la derecha, entonces f es suprayectiva.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 |
import tactic open function variables {α β: Type*} variable {f : α → β} example (hf : has_right_inverse f) : surjective 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 |
import tactic open function variables {α β: Type*} variable {f : α → β} -- 1ª demostración example (hf : has_right_inverse f) : surjective f := begin unfold surjective, unfold has_right_inverse at hf, cases hf with g hg, intro b, use g b, exact hg b, end -- 2ª demostración example (hf : has_right_inverse f) : surjective f := begin intro b, cases hf with g hg, use g b, exact hg b, end -- 3ª demostración example (hf : has_right_inverse f) : surjective f := begin intro b, cases hf with g hg, use [g b, hg b], end -- 4ª demostración example (hf : has_right_inverse f) : surjective f := has_right_inverse.surjective 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 56 57 58 59 60 61 62 63 64 65 66 67 68 |
theory Las_funciones_con_inversa_por_la_derecha_son_suprayectivas imports Main begin definition tiene_inversa_dcha :: "('a ⇒ 'b) ⇒ bool" where "tiene_inversa_dcha f ⟷ (∃g. ∀y. f (g y) = y)" (* 1ª demostración *) lemma assumes "tiene_inversa_dcha f" shows "surj f" proof (unfold surj_def; intro allI) fix y obtain g where "∀y. f (g y) = y" using assms tiene_inversa_dcha_def by auto then have "f (g y) = y" by (rule allE) then have "y = f (g y)" by (rule sym) then show "∃x. y = f x" by (rule exI) qed (* 2ª demostración *) lemma assumes "tiene_inversa_dcha f" shows "surj f" proof (unfold surj_def; intro allI) fix y obtain g where "∀y. f (g y) = y" using assms tiene_inversa_dcha_def by auto then have "y = f (g y)" by simp then show "∃x. y = f x" by (rule exI) qed (* 3ª demostración *) lemma assumes "tiene_inversa_dcha f" shows "surj f" proof (unfold surj_def; intro allI) fix y obtain g where "∀y. f (g y) = y" using assms tiene_inversa_dcha_def by auto then show "∃x. y = f x" by metis qed (* 4ª demostración *) lemma assumes "tiene_inversa_dcha f" shows "surj f" proof (unfold surj_def; intro allI) fix y show "∃x. y = f x" using assms tiene_inversa_dcha_def by metis qed (* 5ª demostración *) lemma assumes "tiene_inversa_dcha f" shows "surj f" using assms tiene_inversa_dcha_def surj_def by metis 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]