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
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 |
theory Imagen_de_la_union imports Main begin section ‹1ª demostración› lemma "f ` (s ∪ t) = f ` s ∪ f ` t" proof (rule equalityI) show "f ` (s ∪ t) ⊆ f ` s ∪ f ` t" proof (rule subsetI) fix y assume "y ∈ f ` (s ∪ t)" then show "y ∈ f ` s ∪ f ` t" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s ∪ t" then show "y ∈ f ` s ∪ f ` t" proof (rule UnE) assume "x ∈ s" with ‹y = f x› have "y ∈ f ` s" by (simp only: image_eqI) then show "y ∈ f ` s ∪ f ` t" by (rule UnI1) next assume "x ∈ t" with ‹y = f x› have "y ∈ f ` t" by (simp only: image_eqI) then show "y ∈ f ` s ∪ f ` t" by (rule UnI2) qed qed qed next show "f ` s ∪ f ` t ⊆ f ` (s ∪ t)" proof (rule subsetI) fix y assume "y ∈ f ` s ∪ f ` t" then show "y ∈ f ` (s ∪ t)" proof (rule UnE) assume "y ∈ f ` s" then show "y ∈ f ` (s ∪ t)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s" then have "x ∈ s ∪ t" by (rule UnI1) with ‹y = f x› show "y ∈ f ` (s ∪ t)" by (simp only: image_eqI) qed next assume "y ∈ f ` t" then show "y ∈ f ` (s ∪ t)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ t" then have "x ∈ s ∪ t" by (rule UnI2) with ‹y = f x› show "y ∈ f ` (s ∪ t)" by (simp only: image_eqI) qed qed qed qed section ‹2ª demostración› lemma "f ` (s ∪ t) = f ` s ∪ f ` t" proof show "f ` (s ∪ t) ⊆ f ` s ∪ f ` t" proof fix y assume "y ∈ f ` (s ∪ t)" then show "y ∈ f ` s ∪ f ` t" proof fix x assume "y = f x" assume "x ∈ s ∪ t" then show "y ∈ f ` s ∪ f ` t" proof assume "x ∈ s" with ‹y = f x› have "y ∈ f ` s" by simp then show "y ∈ f ` s ∪ f ` t" by simp next assume "x ∈ t" with ‹y = f x› have "y ∈ f ` t" by simp then show "y ∈ f ` s ∪ f ` t" by simp qed qed qed next show "f ` s ∪ f ` t ⊆ f ` (s ∪ t)" proof fix y assume "y ∈ f ` s ∪ f ` t" then show "y ∈ f ` (s ∪ t)" proof assume "y ∈ f ` s" then show "y ∈ f ` (s ∪ t)" proof fix x assume "y = f x" assume "x ∈ s" then have "x ∈ s ∪ t" by simp with ‹y = f x› show "y ∈ f ` (s ∪ t)" by simp qed next assume "y ∈ f ` t" then show "y ∈ f ` (s ∪ t)" proof fix x assume "y = f x" assume "x ∈ t" then have "x ∈ s ∪ t" by simp with ‹y = f x› show "y ∈ f ` (s ∪ t)" by simp qed qed qed qed section ‹3ª demostración› lemma "f ` (s ∪ t) = f ` s ∪ f ` t" by (simp only: image_Un) section ‹4ª demostración› lemma "f ` (s ∪ t) = f ` s ∪ f ` t" by auto end |