DAO: La semana en Calculemus (del 2 al 6 de mayo de 2022)
Esta semana he publicado en Calculemus las soluciones de los siguientes problemas:
A continuación se muestran las soluciones.
1. Imagen de la unión
En Lean, la imagen de un conjunto s por una función f se representa por f '' s
; es decir, f '' s = {y | ∃ x, x ∈ s ∧ f x = y}
Demostrar que f '' (s ∪ t) = f '' s ∪ f '' t
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 |
import data.set.basic import tactic open set variables {α : Type*} {β : Type*} variable f : α → β variables s t : set α example : f '' (s ∪ t) = f '' s ∪ f '' t := 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 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 153 154 155 156 157 |
import data.set.basic import tactic open set variables {α : Type*} {β : Type*} variable f : α → β variables s t : set α -- 1ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { intro h, rw mem_image at h, cases h with x hx, cases hx with xst fxy, rw ← fxy, rw mem_union at xst, cases xst with xs xt, { apply mem_union_left, apply mem_image_of_mem, exact xs, }, { apply mem_union_right, apply mem_image_of_mem, exact xt, }}, { intro h, rw mem_union at h, cases h with yfs yft, { rw mem_image, rw mem_image at yfs, cases yfs with x hx, cases hx with xs fxy, use x, split, { apply mem_union_left, exact xs, }, { exact fxy, }}, { rw mem_image, rw mem_image at yft, cases yft with x hx, cases hx with xt fxy, use x, split, { apply mem_union_right, exact xt, }, { exact fxy, }}}, end -- 2ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { rintro ⟨x, xst, rfl⟩, cases xst with xs xt, { left, exact mem_image_of_mem f xs, }, { right, exact mem_image_of_mem f xt, }}, { rintro (yfs | yft), { rcases yfs with ⟨x, xs, rfl⟩, apply mem_image_of_mem, left, exact xs, }, { rcases yft with ⟨x, xt, rfl⟩, apply mem_image_of_mem, right, exact xt, }}, end -- 3ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { rintro ⟨x, xst, rfl⟩, cases xst with xs xt, { left, use [x, xs], }, { right, use [x, xt], }}, { rintro (yfs | yft), { rcases yfs with ⟨x, xs, rfl⟩, use [x, or.inl xs], }, { rcases yft with ⟨x, xt, rfl⟩, use [x, or.inr xt], }}, end -- 4ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { rintro ⟨x, xs | xt, rfl⟩, { left, use [x, xs], }, { right, use [x, xt], }}, { rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩), { use [x, or.inl xs], }, { use [x, or.inr xt], }}, end -- 5ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { rintros ⟨x, xs | xt, rfl⟩ ; finish, }, { rintros (⟨x, xs, rfl⟩ | ⟨x, xt, rfl⟩) ; finish, }, end -- 6ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, split, { finish, }, { finish, }, end -- 7ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := begin ext y, rw iff_def, finish, end -- 8ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := by finish [ext_iff, iff_def] -- 9ª demostración -- =============== example : f '' (s ∪ t) = f '' s ∪ f '' t := -- by library_search image_union f s t |
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
2. 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