Teorema de Cantor
Demostrar el teorema de Cantor; es decir, que no existe ninguna aplicación suprayectiva de un conjunto en su conjunto potencia.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import data.set.basic open function variables {α : Type} example : ∀ f : α → set α, ¬ surjective f := sorry |
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 |
import data.set.basic open function variables {α : Type} -- 1ª demostración -- =============== example : ∀ f : α → set α, ¬ surjective f := begin intros f hf, let S := {i | i ∉ f i}, unfold surjective at hf, cases hf S with j hj, by_cases j ∈ S, { dsimp at h, apply h, rw hj, exact h, }, { apply h, rw ← hj at h, exact h, }, end -- 2ª demostración -- =============== example : ∀ f : α → set α, ¬ surjective f := begin intros f hf, let S := {i | i ∉ f i}, cases hf S with j hj, by_cases j ∈ S, { apply h, rwa hj, }, { apply h, rwa ← hj at h, }, end -- 3ª demostración -- =============== example : ∀ f : α → set α, ¬ surjective f := begin intros f hf, let S := {i | i ∉ f i}, cases hf S with j hj, have h : (j ∈ S) = (j ∉ S), from calc (j ∈ S) = (j ∉ f j) : set.mem_set_of_eq ... = (j ∉ S) : congr_arg not (congr_arg (has_mem.mem j) hj), exact false_of_a_eq_not_a h, end -- 4ª demostración -- =============== example : ∀ f : α → set α, ¬ surjective f := begin intros f hf, let S := {i | i ∉ f i}, cases hf S with j hj, have h : (j ∈ S) = (j ∉ S), { dsimp, exact congr_arg not (congr_arg (has_mem.mem j) hj), }, { exact false_of_a_eq_not_a (congr_arg not (congr_arg not h)), }, end -- 5ª demostración -- =============== example : ∀ f : α → set α, ¬ surjective f := cantor_surjective |
El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.
La construcción de las demostraciones se muestra en el siguiente vídeo
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 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 |
theory Teorema_de_Cantor imports Main begin (* 1ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof (rule notI) assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) show False proof (cases "j ∈ ?S") assume "j ∈ ?S" then have "j ∉ f j" by (rule CollectD) moreover have "j ∈ f j" using ‹?S = f j› ‹j ∈ ?S› by (rule subst) ultimately show False by (rule notE) next assume "j ∉ ?S" with ‹?S = f j› have "j ∉ f j" by (rule subst) then have "j ∈ ?S" by (rule CollectI) with ‹j ∉ ?S› show False by (rule notE) qed qed (* 2ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof (rule notI) assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∉ ?S" proof (rule notI) assume "j ∈ ?S" then have "j ∉ f j" by (rule CollectD) with ‹?S = f j› have "j ∉ ?S" by (rule ssubst) then show False using ‹j ∈ ?S› by (rule notE) qed moreover have "j ∈ ?S" proof (rule CollectI) show "j ∉ f j" proof (rule notI) assume "j ∈ f j" with ‹?S = f j› have "j ∈ ?S" by (rule ssubst) then have "j ∉ f j" by (rule CollectD) then show False using ‹j ∈ f j› by (rule notE) qed qed ultimately show False by (rule notE) qed (* 3ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∉ ?S" proof assume "j ∈ ?S" then have "j ∉ f j" by simp with ‹?S = f j› have "j ∉ ?S" by simp then show False using ‹j ∈ ?S› by simp qed moreover have "j ∈ ?S" proof show "j ∉ f j" proof assume "j ∈ f j" with ‹?S = f j› have "j ∈ ?S" by simp then have "j ∉ f j" by simp then show False using ‹j ∈ f j› by simp qed qed ultimately show False by simp qed (* 4ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof (rule notI) assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∈ ?S = (j ∉ f j)" by (rule mem_Collect_eq) also have "… = (j ∉ ?S)" by (simp only: ‹?S = f j›) finally show False by (simp only: simp_thms(10)) qed (* 5ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" proof assume "surj f" let ?S = "{i. i ∉ f i}" have "∃ j. ?S = f j" using ‹surj f› by (simp only: surjD) then obtain j where "?S = f j" by (rule exE) have "j ∈ ?S = (j ∉ f j)" by simp also have "… = (j ∉ ?S)" using ‹?S = f j› by simp finally show False by simp qed (* 6ª demostración *) theorem fixes f :: "'α ⇒ 'α set" shows "¬ surj f" unfolding surj_def by best end |