La composición de funciones inyectivas es inyectiva
Demostrar que la composición de dos funciones inyectivas es una función inyectiva.
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 : injective f) (Hg : injective g) : injective (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 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 97 |
import tactic open function variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} -- 1ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := begin intros x y h, apply Hf, apply Hg, exact h, end -- 2ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := begin intros x y h, apply Hf, exact Hg h, end -- 3ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := begin intros x y h, exact Hf (Hg h), end -- 4ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := λ x y h, Hf (Hg h) -- 5ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := assume x y, assume h1 : (g ∘ f) x = (g ∘ f) y, have h2 : f x = f y, from Hg h1, show x = y, from Hf h2 -- 6ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := assume x y, assume h1 : (g ∘ f) x = (g ∘ f) y, show x = y, from Hf (Hg h1) -- 7ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := assume x y, assume h1 : (g ∘ f) x = (g ∘ f) y, Hf (Hg h1) -- 8ª demostración example (Hf : injective f) (Hg : injective g) : injective (g ∘ f) := λ x y h1, Hf (Hg h1) -- 9ª demostración example (Hg : injective g) (Hf : injective f) : injective (g ∘ f) := -- by library_search injective.comp Hg Hf -- 10ª demostración example (Hg : injective g) (Hf : injective f) : injective (g ∘ f) := -- by hint by tauto |
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 |
theory La_composicion_de_funciones_inyectivas_es_inyectiva imports Main begin (* 1ª demostración *) lemma assumes "inj f" "inj g" shows "inj (f ∘ g)" proof (rule injI) fix x y assume "(f ∘ g) x = (f ∘ g) y" then have "f (g x) = f (g y)" by (simp only: o_apply) then have "g x = g y" using ‹inj f› by (simp only: injD) then show "x = y" using ‹inj g› by (simp only: injD) qed (* 2ª demostración *) lemma assumes "inj f" "inj g" shows "inj (f ∘ g)" using assms by (simp add: inj_def) (* 3ª demostración *) lemma assumes "inj f" "inj g" shows "inj (f ∘ g)" using assms by (rule inj_compose) 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]