La composición de funciones biyectivas es biyectiva
Demostrar que la composición de dos funciones biyectivas es una función biyectiva.
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 : bijective f) (Hg : bijective g) : bijective (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 |
import tactic open function variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} -- 1ª demostración example (Hf : bijective f) (Hg : bijective g) : bijective (g ∘ f) := begin cases Hf with Hfi Hfs, cases Hg with Hgi Hgs, split, { apply injective.comp, { exact Hgi, }, { exact Hfi, }}, { apply surjective.comp, { exact Hgs, }, { exact Hfs, }}, end -- 2ª demostración example (Hf : bijective f) (Hg : bijective g) : bijective (g ∘ f) := begin cases Hf with Hfi Hfs, cases Hg with Hgi Hgs, split, { exact injective.comp Hgi Hfi, }, { exact surjective.comp Hgs Hfs, }, end -- 3ª demostración example (Hf : bijective f) (Hg : bijective g) : bijective (g ∘ f) := begin cases Hf with Hfi Hfs, cases Hg with Hgi Hgs, exact ⟨injective.comp Hgi Hfi, surjective.comp Hgs Hfs⟩, end -- 4ª demostración example : bijective f → bijective g → bijective (g ∘ f) := begin rintros ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩, exact ⟨injective.comp Hgi Hfi, surjective.comp Hgs Hfs⟩, end -- 5ª demostración example : bijective f → bijective g → bijective (g ∘ f) := λ ⟨Hfi, Hfs⟩ ⟨Hgi, Hgs⟩, ⟨injective.comp Hgi Hfi, surjective.comp Hgs Hfs⟩ -- 6ª demostración example (Hf : bijective f) (Hg : bijective g) : bijective (g ∘ f) := -- by library_search bijective.comp Hg 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 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 |
theory La_composicion_de_funciones_biyectivas_es_biyectiva imports Main begin (* 1ª demostración *) lemma assumes "bij f" "bij g" shows "bij (g ∘ f)" proof (rule bijI) show "inj (g ∘ f)" proof (rule inj_compose) show "inj g" using ‹bij g› by (rule bij_is_inj) next show "inj f" using ‹bij f› by (rule bij_is_inj) qed next show "surj (g ∘ f)" proof (rule comp_surj) show "surj f" using ‹bij f› by (rule bij_is_surj) next show "surj g" using ‹bij g› by (rule bij_is_surj) qed qed (* 2ª demostración *) lemma assumes "bij f" "bij g" shows "bij (g ∘ f)" proof (rule bijI) show "inj (g ∘ f)" proof (rule inj_compose) show "inj g" by (rule bij_is_inj [OF ‹bij g›]) next show "inj f" by (rule bij_is_inj [OF ‹bij f›]) qed next show "surj (g ∘ f)" proof (rule comp_surj) show "surj f" by (rule bij_is_surj [OF ‹bij f›]) next show "surj g" by (rule bij_is_surj [OF ‹bij g›]) qed qed (* 3ª demostración *) lemma assumes "bij f" "bij g" shows "bij (g ∘ f)" proof (rule bijI) show "inj (g ∘ f)" by (rule inj_compose [OF bij_is_inj [OF ‹bij g›] bij_is_inj [OF ‹bij f›]]) next show "surj (g ∘ f)" by (rule comp_surj [OF bij_is_surj [OF ‹bij f›] bij_is_surj [OF ‹bij g›]]) qed (* 4ª demostración *) lemma assumes "bij f" "bij g" shows "bij (g ∘ f)" by (rule bijI [OF inj_compose [OF bij_is_inj [OF ‹bij g›] bij_is_inj [OF ‹bij f›]] comp_surj [OF bij_is_surj [OF ‹bij f›] bij_is_surj [OF ‹bij g›]]]) (* 5ª demostración *) lemma assumes "bij f" "bij g" shows "bij (g ∘ f)" using assms by (rule bij_comp) 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]