La composición de funciones suprayectivas es suprayectiva
Demostrar que la composición de dos funciones suprayectivas es una función suprayectiva.
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 variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} example (hf : surjective f) (hg : surjective g) : surjective (g ∘ 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 |
import tactic open function variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} -- 1ª demostración example (hf : surjective f) (hg : surjective g) : surjective (g ∘ f) := begin intro z, cases hg z with y hy, cases hf y with x hx, use x, dsimp, rw hx, exact hy, end -- 2ª demostración example (hf : surjective f) (hg : surjective g) : surjective (g ∘ f) := begin intro z, cases hg z with y hy, cases hf y with x hx, use x, calc (g ∘ f) x = g (f x) : by rw comp_app ... = g y : congr_arg g hx ... = z : hy, end -- 3ª demostración example (hf : surjective f) (hg : surjective g) : surjective (g ∘ f) := assume z, exists.elim (hg z) ( assume y (hy : g y = z), exists.elim (hf y) ( assume x (hx : f x = y), have g (f x) = z, from eq.subst (eq.symm hx) hy, show ∃ x, g (f x) = z, from exists.intro x this)) -- 4ª demostración example (hf : surjective f) (hg : surjective g) : surjective (g ∘ f) := -- by library_search surjective.comp hg hf -- 5ª demostración example (hf : surjective f) (hg : surjective g) : surjective (g ∘ f) := λ z, exists.elim (hg z) (λ y hy, exists.elim (hf y) (λ x hx, exists.intro x (show g (f x) = z, from (eq.trans (congr_arg g hx) hy)))) |
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 |
theory La_composicion_de_funciones_suprayectivas_es_suprayectiva imports Main begin (* 1ª demostración *) lemma assumes "surj (f :: 'a ⇒ 'b)" "surj (g :: 'b ⇒ 'c)" shows "surj (g ∘ f)" proof (unfold surj_def; intro allI) fix z obtain y where hy : "g y = z" using ‹surj g› by (metis surjD) obtain x where hx : "f x = y" using ‹surj f› by (metis surjD) have "(g ∘ f) x = g (f x)" by (simp only: o_apply) also have "… = g y" by (simp only: ‹f x = y›) also have "… = z" by (simp only: ‹g y = z›) finally have "(g ∘ f) x = z" by this then have "z = (g ∘ f) x" by (rule sym) then show "∃x. z = (g ∘ f) x" by (rule exI) qed (* 2ª demostración *) lemma assumes "surj f" "surj g" shows "surj (g ∘ f)" using assms image_comp [of g f UNIV] by (simp only:) (* 3ª demostración *) lemma assumes "surj f" "surj g" shows "surj (g ∘ f)" using assms by (rule comp_surj) 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]