La semana en Calculemus (27 de abril de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:
- 1. Unión con la imagen
- 2. Intersección con la imagen
- 3. Unión con la imagen inversa
- 4. Imagen de la unión general
- 5. Imagen de la intersección general
A continuación se muestran las soluciones.
1. Unión con la imagen
Demostrar con Lean4 que
\[ f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable (α β : Type _) variable (f : α → β) variable (s : Set α) variable (v : Set β) example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v := by sorry |
1.1. Demostración en lenguaje natural
Sea \(y ∈ f[s ∪ f⁻¹[v]]\). Entonces, existe un x tal que
\begin{align}
&x ∈ s ∪ f⁻¹[v] \tag{1} \\
&f(x) = y \tag{2}
\end{align}
De (1), se tiene que \(x ∈ s\) ó \(x ∈ f⁻¹[v]\). Vamos a demostrar en ambos casos que
\[ y ∈ f[s] ∪ v \]
Caso 1: Supongamos que \(x ∈ s\). Entonces,
\[ f(x) ∈ f[s] \]
y, por (2), se tiene que
\[ y ∈ f[s] \]
Por tanto,
\[ y ∈ f[s] ∪ v \]
Caso 2: Supongamos que \(x ∈ f⁻¹[v]\). Entonces,
\[ f(x) ∈ v \]
y, por (2), se tiene que
\[ y ∈ v \]
Por tanto,
\[ y ∈ f[s] ∪ v \]
1.2. Demostraciones con Lean4
|
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 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable (α β : Type _) variable (f : α → β) variable (s : Set α) variable (v : Set β) -- 1ª demostración -- =============== example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v := by intros y hy obtain ⟨x : α, hx : x ∈ s ∪ f ⁻¹' v ∧ f x = y⟩ := hy obtain ⟨hx1 : x ∈ s ∪ f ⁻¹' v, fxy : f x = y⟩ := hx cases' hx1 with xs xv . -- xs : x ∈ s have h1 : f x ∈ f '' s := mem_image_of_mem f xs have h2 : y ∈ f '' s := by rwa [fxy] at h1 show y ∈ f '' s ∪ v exact mem_union_left v h2 . -- xv : x ∈ f ⁻¹' v have h3 : f x ∈ v := mem_preimage.mp xv have h4 : y ∈ v := by rwa [fxy] at h3 show y ∈ f '' s ∪ v exact mem_union_right (f '' s) h4 -- 1ª demostración -- =============== example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v := by intros y hy obtain ⟨x : α, hx : x ∈ s ∪ f ⁻¹' v ∧ f x = y⟩ := hy obtain ⟨hx1 : x ∈ s ∪ f ⁻¹' v, fxy : f x = y⟩ := hx cases' hx1 with xs xv . -- xs : x ∈ s left -- ⊢ y ∈ f '' s use x -- ⊢ x ∈ s ∧ f x = y constructor . -- ⊢ x ∈ s exact xs . -- ⊢ f x = y exact fxy . -- ⊢ y ∈ f '' s ∪ v right -- ⊢ y ∈ v rw [←fxy] -- ⊢ f x ∈ v exact xv -- 2ª demostración -- =============== example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v := by rintro y ⟨x, xs | xv, fxy⟩ -- y : β -- x : α . -- xs : x ∈ s -- ⊢ y ∈ f '' s ∪ v left -- ⊢ y ∈ f '' s use x, xs -- ⊢ f x = y exact fxy . -- xv : x ∈ f ⁻¹' v -- ⊢ y ∈ f '' s ∪ v right -- ⊢ y ∈ v rw [←fxy] -- ⊢ f x ∈ v exact xv -- 3ª demostración -- =============== example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v := by rintro y ⟨x, xs | xv, fxy⟩ <;> aesop -- Lemas usados -- ============ -- variable (x : α) -- variable (t : Set α) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) -- #check (mem_preimage : x ∈ f ⁻¹' v ↔ f x ∈ v) -- #check (mem_union_left t : x ∈ s → x ∈ s ∪ t) -- #check (mem_union_right s : x ∈ t → x ∈ s ∪ t) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
1.3. Demostraciones 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 |
theory Union_con_la_imagen imports Main begin (* 1ª demostración *) lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v" proof (rule subsetI) fix y assume "y ∈ f ` (s ∪ f -` v)" then show "y ∈ f ` s ∪ v" proof (rule imageE) fix x assume "y = f x" assume "x ∈ s ∪ f -` v" then show "y ∈ f ` s ∪ v" proof (rule UnE) assume "x ∈ s" then have "f x ∈ f ` s" by (rule imageI) with ‹y = f x› have "y ∈ f ` s" by (rule ssubst) then show "y ∈ f ` s ∪ v" by (rule UnI1) next assume "x ∈ f -` v" then have "f x ∈ v" by (rule vimageD) with ‹y = f x› have "y ∈ v" by (rule ssubst) then show "y ∈ f ` s ∪ v" by (rule UnI2) qed qed qed (* 2ª demostración *) lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v" proof fix y assume "y ∈ f ` (s ∪ f -` v)" then show "y ∈ f ` s ∪ v" proof fix x assume "y = f x" assume "x ∈ s ∪ f -` v" then show "y ∈ f ` s ∪ v" proof assume "x ∈ s" then have "f x ∈ f ` s" by simp with ‹y = f x› have "y ∈ f ` s" by simp then show "y ∈ f ` s ∪ v" by simp next assume "x ∈ f -` v" then have "f x ∈ v" by simp with ‹y = f x› have "y ∈ v" by simp then show "y ∈ f ` s ∪ v" by simp qed qed qed (* 3ª demostración *) lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v" proof fix y assume "y ∈ f ` (s ∪ f -` v)" then show "y ∈ f ` s ∪ v" proof fix x assume "y = f x" assume "x ∈ s ∪ f -` v" then show "y ∈ f ` s ∪ v" proof assume "x ∈ s" then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›) next assume "x ∈ f -` v" then show "y ∈ f ` s ∪ v" by (simp add: ‹y = f x›) qed qed qed (* 4ª demostración *) lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v" proof fix y assume "y ∈ f ` (s ∪ f -` v)" then show "y ∈ f ` s ∪ v" proof fix x assume "y = f x" assume "x ∈ s ∪ f -` v" then show "y ∈ f ` s ∪ v" using ‹y = f x› by blast qed qed (* 5ª demostración *) lemma "f ` (s ∪ f -` u) ⊆ f ` s ∪ u" by auto end |
2. Intersección con la imagen
Demostrar con Lean4 que
\[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (v : Set β) example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by sorry |
2.1. Demostración en lenguaje natural
Tenemmos que demostrar que, para todo \(y\),
\[ y ∈ f[s] ∩ v ↔ y ∈ f[s ∩ f⁻¹[v]] \]
Lo haremos demostrando las dos implicaciones.
(⟹) Supongamos que \(y ∈ f[s] ∩ v\). Entonces,
\begin{align}
&y ∈ f[s] \tag{1} \\
&y ∈ v \tag{2}
\end{align}
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ s \tag{3} \\
&f(x) = y \tag{4}
\end{align}
De (2) y (4), se tiene que
\[ f(x) ∈ v \]
y, por tanto,
\[ x ∈ f⁻¹[v] \tag{5} \]
De (3) y (5), se tiene que
\[ x ∈ s ∩ f⁻¹[v] \]
Por tanto,
\[ f(x) ∈ f[s ∩ f⁻¹[v]] \]
y, por (4),
\[ y ∈ f[s ∩ f⁻¹[v]] \]
(⟸) Supongamos que \(y ∈ f[s ∩ f⁻¹[v]]\). Entonces, existe un \(x\) tal que
\begin{align}
&x ∈ s ∩ f⁻¹[v] \tag{6} \\
&f(x) = y \tag{7}
\end{align}
Por (6), se tiene que
\begin{align}
&x ∈ s \tag{8} \\
&x ∈ f⁻¹[v] \tag{9}
\end{align}
Por (8), se tiene que
\[ f(x) ∈ f[s] \]
y, por (7),
\[ y ∈ f[s] \tag{10} \]
Por (9),
\[ f(x) ∈ v \]
y, por (7),
\[ y ∈ v \tag{11} \]
Por (10) y (11),
\[ y ∈ f[s] ∩ v \]
2.2. Demostraciones con Lean4
|
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 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 |
import Mathlib.Data.Set.Function import Mathlib.Tactic open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (v : Set β) -- 1ª demostración -- =============== example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ v ↔ y ∈ f '' (s ∩ f ⁻¹' v) constructor . -- ⊢ y ∈ f '' s ∩ v → y ∈ f '' (s ∩ f ⁻¹' v) intro hy -- hy : y ∈ f '' s ∩ v -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) cases' hy with hyfs yv -- hyfs : y ∈ f '' s -- yv : y ∈ v cases' hyfs with x hx -- x : α -- hx : x ∈ s ∧ f x = y cases' hx with xs fxy -- xs : x ∈ s -- fxy : f x = y have h1 : f x ∈ v := by rwa [←fxy] at yv have h3 : x ∈ s ∩ f ⁻¹' v := mem_inter xs h1 have h4 : f x ∈ f '' (s ∩ f ⁻¹' v) := mem_image_of_mem f h3 show y ∈ f '' (s ∩ f ⁻¹' v) rwa [fxy] at h4 . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) → y ∈ f '' s ∩ v intro hy -- hy : y ∈ f '' (s ∩ f ⁻¹' v) -- ⊢ y ∈ f '' s ∩ v cases' hy with x hx -- x : α -- hx : x ∈ s ∩ f ⁻¹' v ∧ f x = y cases' hx with hx1 fxy -- hx1 : x ∈ s ∩ f ⁻¹' v -- fxy : f x = y cases' hx1 with xs xfv -- xs : x ∈ s -- xfv : x ∈ f ⁻¹' v have h5 : f x ∈ f '' s := mem_image_of_mem f xs have h6 : y ∈ f '' s := by rwa [fxy] at h5 have h7 : f x ∈ v := mem_preimage.mp xfv have h8 : y ∈ v := by rwa [fxy] at h7 show y ∈ f '' s ∩ v exact mem_inter h6 h8 -- 2ª demostración -- =============== example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ v ↔ y ∈ f '' (s ∩ f ⁻¹' v) constructor . -- ⊢ y ∈ f '' s ∩ v → y ∈ f '' (s ∩ f ⁻¹' v) intro hy -- hy : y ∈ f '' s ∩ v -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) cases' hy with hyfs yv -- hyfs : y ∈ f '' s -- yv : y ∈ v cases' hyfs with x hx -- x : α -- hx : x ∈ s ∧ f x = y cases' hx with xs fxy -- xs : x ∈ s -- fxy : f x = y use x -- ⊢ x ∈ s ∩ f ⁻¹' v ∧ f x = y constructor . -- ⊢ x ∈ s ∩ f ⁻¹' v constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ f ⁻¹' v rw [mem_preimage] -- ⊢ f x ∈ v rw [fxy] -- ⊢ y ∈ v exact yv . -- ⊢ f x = y exact fxy . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) → y ∈ f '' s ∩ v intro hy -- hy : y ∈ f '' (s ∩ f ⁻¹' v) -- ⊢ y ∈ f '' s ∩ v cases' hy with x hx -- x : α -- hx : x ∈ s ∩ f ⁻¹' v ∧ f x = y constructor . -- ⊢ y ∈ f '' s use x -- ⊢ x ∈ s ∧ f x = y constructor . -- ⊢ x ∈ s exact hx.1.1 . -- ⊢ f x = y exact hx.2 . -- ⊢ y ∈ v cases' hx with hx1 fxy -- hx1 : x ∈ s ∩ f ⁻¹' v -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ v rw [←mem_preimage] -- ⊢ x ∈ f ⁻¹' v exact hx1.2 -- 3ª demostración -- =============== example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ v ↔ y ∈ f '' (s ∩ f ⁻¹' v) constructor . -- ⊢ y ∈ f '' s ∩ v → y ∈ f '' (s ∩ f ⁻¹' v) rintro ⟨⟨x, xs, fxy⟩, yv⟩ -- yv : y ∈ v -- x : α -- xs : x ∈ s -- fxy : f x = y -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) use x -- ⊢ x ∈ s ∩ f ⁻¹' v ∧ f x = y constructor . -- ⊢ x ∈ s ∩ f ⁻¹' v constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ f ⁻¹' v rw [mem_preimage] -- ⊢ f x ∈ v rw [fxy] -- ⊢ y ∈ v exact yv . exact fxy . rintro ⟨x, ⟨xs, xv⟩, fxy⟩ -- x : α -- fxy : f x = y -- xs : x ∈ s -- xv : x ∈ f ⁻¹' v -- ⊢ y ∈ f '' s ∩ v constructor . -- ⊢ y ∈ f '' s use x, xs -- ⊢ f x = y exact fxy . -- ⊢ y ∈ v rw [←fxy] -- ⊢ f x ∈ v rw [←mem_preimage] -- ⊢ x ∈ f ⁻¹' v exact xv -- 4ª demostración -- =============== example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by ext y -- y : β -- ⊢ y ∈ f '' s ∩ v ↔ y ∈ f '' (s ∩ f ⁻¹' v) constructor . -- ⊢ y ∈ f '' s ∩ v → y ∈ f '' (s ∩ f ⁻¹' v) rintro ⟨⟨x, xs, fxy⟩, yv⟩ -- yv : y ∈ v -- x : α -- xs : x ∈ s -- fxy : f x = y -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) aesop . -- ⊢ y ∈ f '' (s ∩ f ⁻¹' v) → y ∈ f '' s ∩ v rintro ⟨x, ⟨xs, xv⟩, fxy⟩ -- x : α -- fxy : f x = y -- xs : x ∈ s -- xv : x ∈ f ⁻¹' v -- ⊢ y ∈ f '' s ∩ v aesop -- 5ª demostración -- =============== example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := by ext ; constructor <;> aesop -- 6ª demostración -- =============== example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) := (image_inter_preimage f s v).symm -- Lemas usados -- ============ -- variable (x : α) -- variable (a b : Set α) -- #check (image_inter_preimage f s v : f '' (s ∩ f ⁻¹' v) = f '' s ∩ v) -- #check (mem_image_of_mem f : x ∈ a → f x ∈ f '' a) -- #check (mem_inter : x ∈ a → x ∈ b → x ∈ a ∩ b) -- #check (mem_preimage : x ∈ f ⁻¹' v ↔ f x ∈ v) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
2.3. Demostraciones 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 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 |
theory Interseccion_con_la_imagen_inversa imports Main begin (* 1ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" proof (rule equalityI) show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)" proof (rule subsetI) fix y assume "y ∈ (f ` s) ∩ v" then show "y ∈ f ` (s ∩ f -` v)" proof (rule IntE) assume "y ∈ v" assume "y ∈ f ` s" then show "y ∈ f ` (s ∩ f -` v)" proof (rule imageE) fix x assume "x ∈ s" assume "y = f x" then have "f x ∈ v" using ‹y ∈ v› by (rule subst) then have "x ∈ f -` v" by (rule vimageI2) with ‹x ∈ s› have "x ∈ s ∩ f -` v" by (rule IntI) then have "f x ∈ f ` (s ∩ f -` v)" by (rule imageI) with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by (rule ssubst) qed qed qed next show "f ` (s ∩ f -` v) ⊆ (f ` s) ∩ v" proof (rule subsetI) fix y assume "y ∈ f ` (s ∩ f -` v)" then show "y ∈ (f ` s) ∩ v" proof (rule imageE) fix x assume "y = f x" assume hx : "x ∈ s ∩ f -` v" have "y ∈ f ` s" proof - have "x ∈ s" using hx by (rule IntD1) then have "f x ∈ f ` s" by (rule imageI) with ‹y = f x› show "y ∈ f ` s" by (rule ssubst) qed moreover have "y ∈ v" proof - have "x ∈ f -` v" using hx by (rule IntD2) then have "f x ∈ v" by (rule vimageD) with ‹y = f x› show "y ∈ v" by (rule ssubst) qed ultimately show "y ∈ (f ` s) ∩ v" by (rule IntI) qed qed qed (* 2ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" proof show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)" proof fix y assume "y ∈ (f ` s) ∩ v" then show "y ∈ f ` (s ∩ f -` v)" proof assume "y ∈ v" assume "y ∈ f ` s" then show "y ∈ f ` (s ∩ f -` v)" proof fix x assume "x ∈ s" assume "y = f x" then have "f x ∈ v" using ‹y ∈ v› by simp then have "x ∈ f -` v" by simp with ‹x ∈ s› have "x ∈ s ∩ f -` v" by simp then have "f x ∈ f ` (s ∩ f -` v)" by simp with ‹y = f x› show "y ∈ f ` (s ∩ f -` v)" by simp qed qed qed next show "f ` (s ∩ f -` v) ⊆ (f ` s) ∩ v" proof fix y assume "y ∈ f ` (s ∩ f -` v)" then show "y ∈ (f ` s) ∩ v" proof fix x assume "y = f x" assume hx : "x ∈ s ∩ f -` v" have "y ∈ f ` s" proof - have "x ∈ s" using hx by simp then have "f x ∈ f ` s" by simp with ‹y = f x› show "y ∈ f ` s" by simp qed moreover have "y ∈ v" proof - have "x ∈ f -` v" using hx by simp then have "f x ∈ v" by simp with ‹y = f x› show "y ∈ v" by simp qed ultimately show "y ∈ (f ` s) ∩ v" by simp qed qed qed (* 2ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" proof show "(f ` s) ∩ v ⊆ f ` (s ∩ f -` v)" proof fix y assume "y ∈ (f ` s) ∩ v" then show "y ∈ f ` (s ∩ f -` v)" proof assume "y ∈ v" assume "y ∈ f ` s" then show "y ∈ f ` (s ∩ f -` v)" proof fix x assume "x ∈ s" assume "y = f x" then show "y ∈ f ` (s ∩ f -` v)" using ‹x ∈ s› ‹y ∈ v› by simp qed qed qed next show "f ` (s ∩ f -` v) ⊆ (f ` s) ∩ v" proof fix y assume "y ∈ f ` (s ∩ f -` v)" then show "y ∈ (f ` s) ∩ v" proof fix x assume "y = f x" assume hx : "x ∈ s ∩ f -` v" then have "y ∈ f ` s" using ‹y = f x› by simp moreover have "y ∈ v" using hx ‹y = f x› by simp ultimately show "y ∈ (f ` s) ∩ v" by simp qed qed qed (* 4ª demostración *) lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)" by auto end |
3. Unión con la imagen inversa
Demostrar con Lean4 que
\[ s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (v : Set β) example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by sorry |
3.1. Demostración en lenguaje natural
Sea \(x ∈ s ∪ f⁻¹[v]\). Entonces, se pueden dar dos casos.
Caso 1: Supongamos que \(x ∈ s\). Entonces, se tiene
\begin{align}
&f(x) ∈ f[s] \\
&f(x) ∈ f[s] ∪ v \\
&x ∈ f⁻¹[f[s] ∪ v]
\end{align}
Caso 2: Supongamos que x ∈ f⁻¹[v]. Entonces, se tiene
\begin{align}
&f(x) ∈ v \\
&f(x) ∈ f[s] ∪ v \\
&x ∈ f⁻¹[f[s] ∪ v]
\end{align}
3.2. Demostraciones con Lean4
|
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 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (s : Set α) variable (v : Set β) -- 1ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by intros x hx -- x : α -- hx : x ∈ s ∪ f ⁻¹' v -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) cases' hx with xs xv . -- xs : x ∈ s have h1 : f x ∈ f '' s := mem_image_of_mem f xs have h2 : f x ∈ f '' s ∪ v := mem_union_left v h1 show x ∈ f ⁻¹' (f '' s ∪ v) exact mem_preimage.mpr h2 . -- xv : x ∈ f ⁻¹' v have h3 : f x ∈ v := mem_preimage.mp xv have h4 : f x ∈ f '' s ∪ v := mem_union_right (f '' s) h3 show x ∈ f ⁻¹' (f '' s ∪ v) exact mem_preimage.mpr h4 -- 2ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by intros x hx -- x : α -- hx : x ∈ s ∪ f ⁻¹' v -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) rw [mem_preimage] -- ⊢ f x ∈ f '' s ∪ v cases' hx with xs xv . -- xs : x ∈ s apply mem_union_left -- ⊢ f x ∈ f '' s apply mem_image_of_mem -- ⊢ x ∈ s exact xs . -- xv : x ∈ f ⁻¹' v apply mem_union_right -- ⊢ f x ∈ v rw [←mem_preimage] -- ⊢ x ∈ f ⁻¹' v exact xv -- 3ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by intros x hx -- x : α -- hx : x ∈ s ∪ f ⁻¹' v -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) cases' hx with xs xv . -- xs : x ∈ s rw [mem_preimage] -- ⊢ f x ∈ f '' s ∪ v apply mem_union_left -- ⊢ f x ∈ f '' s apply mem_image_of_mem -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) rw [mem_preimage] -- ⊢ f x ∈ f '' s ∪ v apply mem_union_right -- ⊢ f x ∈ v exact xv -- 4ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by rintro x (xs | xv) -- x : α -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) . -- xs : x ∈ s left -- ⊢ f x ∈ f '' s exact mem_image_of_mem f xs . -- xv : x ∈ f ⁻¹' v right -- ⊢ f x ∈ v exact xv -- 5ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by rintro x (xs | xv) -- x : α -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) . -- xs : x ∈ s exact Or.inl (mem_image_of_mem f xs) . -- xv : x ∈ f ⁻¹' v exact Or.inr xv -- 5ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := by intros x h -- x : α -- h : x ∈ s ∪ f ⁻¹' v -- ⊢ x ∈ f ⁻¹' (f '' s ∪ v) exact Or.elim h (fun xs ↦ Or.inl (mem_image_of_mem f xs)) Or.inr -- 6ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := fun _ h ↦ Or.elim h (fun xs ↦ Or.inl (mem_image_of_mem f xs)) Or.inr -- 7ª demostración -- =============== example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) := union_preimage_subset s v f -- Lemas usados -- ============ -- variable (x : α) -- variable (t : Set α) -- variable (a b c : Prop) -- #check (Or.elim : a ∨ b → (a → c) → (b → c) → c) -- #check (Or.inl : a → a ∨ b) -- #check (Or.inr : b → a ∨ b) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) -- #check (mem_preimage : x ∈ f ⁻¹' v ↔ f x ∈ v) -- #check (mem_union_left t : x ∈ s → x ∈ s ∪ t) -- #check (mem_union_right s : x ∈ t → x ∈ s ∪ t) -- #check (union_preimage_subset s v f : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3.3. Demostraciones 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 |
theory Union_con_la_imagen_inversa imports Main begin (* 1ª demostración *) lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)" proof (rule subsetI) fix x assume "x ∈ s ∪ f -` v" then have "f x ∈ f ` s ∪ v" proof (rule UnE) assume "x ∈ s" then have "f x ∈ f ` s" by (rule imageI) then show "f x ∈ f ` s ∪ v" by (rule UnI1) next assume "x ∈ f -` v" then have "f x ∈ v" by (rule vimageD) then show "f x ∈ f ` s ∪ v" by (rule UnI2) qed then show "x ∈ f -` (f ` s ∪ v)" by (rule vimageI2) qed (* 2ª demostración *) lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)" proof fix x assume "x ∈ s ∪ f -` v" then have "f x ∈ f ` s ∪ v" proof assume "x ∈ s" then have "f x ∈ f ` s" by simp then show "f x ∈ f ` s ∪ v" by simp next assume "x ∈ f -` v" then have "f x ∈ v" by simp then show "f x ∈ f ` s ∪ v" by simp qed then show "x ∈ f -` (f ` s ∪ v)" by simp qed (* 3ª demostración *) lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)" proof fix x assume "x ∈ s ∪ f -` v" then have "f x ∈ f ` s ∪ v" proof assume "x ∈ s" then show "f x ∈ f ` s ∪ v" by simp next assume "x ∈ f -` v" then show "f x ∈ f ` s ∪ v" by simp qed then show "x ∈ f -` (f ` s ∪ v)" by simp qed (* 4ª demostración *) lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)" by auto end |
4. Imagen de la unión general
Demostrar con Lean4 que
\[ f[⋃ᵢAᵢ] = ⋃ᵢf[Aᵢ] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (A : ℕ → Set α) example : f '' (⋃ i, A i) = ⋃ i, f '' A i := by sorry |
4.1. Demostración en lenguaje natural
Tenemos que demostrar que, para todo \(y\),
\[ y ∈ f[⋃ᵢAᵢ] ↔ y ∈ ⋃ᵢf[Aᵢ] \]
Lo haremos demostrando las dos implicaciones.
(⟹) Supongamos que \(y ∈ f[⋃ᵢAᵢ]\). Entonces, existe un \(x\) tal que
\begin{align}
&x ∈ ⋃ᵢAᵢ \tag{1} \\
&f(x) = y \tag{2}
\end{align}
Por (1), existe un i tal que
\begin{align}
&i ∈ ℕ \tag{3} \\
&x ∈ Aᵢ \tag{4}
\end{align}
Por (4),
\[ f(x) ∈ f[Aᵢ] \]
Por (3),
\[ f(x) ∈ ⋃ᵢf[Aᵢ] \]
y, por (2),
\[ y ∈ ⋃ᵢf[Aᵢ] \]
(⟸) Supongamos que \(y ∈ ⋃ᵢf[Aᵢ]\). Entonces, existe un \(i\) tal que
\begin{align}
&i ∈ ℕ \tag{5} \\
&y ∈ f[Aᵢ] \tag{6}
\end{align}
Por (6), existe un \(x\) tal que
\begin{align}
&x ∈ Aᵢ \tag{7} \\
&f(x) = y \tag{8}
\end{align}
Por (5) y (7),
\[ x ∈ ⋃ᵢAᵢ \]
Luego,
\[ f(x) ∈ f[⋃ᵢAᵢ] \]
y, por (8),
\[ y ∈ f[⋃ᵢAᵢ] \]
4.2. Demostraciones con Lean4
|
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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (A : ℕ → Set α) -- 1ª demostración -- =============== example : f '' (⋃ i, A i) = ⋃ i, f '' A i := by ext y -- y : β -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i ↔ y ∈ ⋃ (i : ℕ), f '' A i constructor . -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i → y ∈ ⋃ (i : ℕ), f '' A i intro hy -- hy : y ∈ f '' ⋃ (i : ℕ), A i -- ⊢ y ∈ ⋃ (i : ℕ), f '' A i have h1 : ∃ x, x ∈ ⋃ i, A i ∧ f x = y := (mem_image f (⋃ i, A i) y).mp hy obtain ⟨x, hx : x ∈ ⋃ i, A i ∧ f x = y⟩ := h1 have xUA : x ∈ ⋃ i, A i := hx.1 have fxy : f x = y := hx.2 have xUA : ∃ i, x ∈ A i := mem_iUnion.mp xUA obtain ⟨i, xAi : x ∈ A i⟩ := xUA have h2 : f x ∈ f '' A i := mem_image_of_mem f xAi have h3 : f x ∈ ⋃ i, f '' A i := mem_iUnion_of_mem i h2 show y ∈ ⋃ i, f '' A i rwa [fxy] at h3 . -- ⊢ y ∈ ⋃ (i : ℕ), f '' A i → y ∈ f '' ⋃ (i : ℕ), A i intro hy -- hy : y ∈ ⋃ (i : ℕ), f '' A i -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i have h4 : ∃ i, y ∈ f '' A i := mem_iUnion.mp hy obtain ⟨i, h5 : y ∈ f '' A i⟩ := h4 have h6 : ∃ x, x ∈ A i ∧ f x = y := (mem_image f (A i) y).mp h5 obtain ⟨x, h7 : x ∈ A i ∧ f x = y⟩ := h6 have h8 : x ∈ A i := h7.1 have h9 : x ∈ ⋃ i, A i := mem_iUnion_of_mem i h8 have h10 : f x ∈ f '' (⋃ i, A i) := mem_image_of_mem f h9 show y ∈ f '' (⋃ i, A i) rwa [h7.2] at h10 -- 2ª demostración -- =============== example : f '' (⋃ i, A i) = ⋃ i, f '' A i := by ext y -- y : β -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i ↔ y ∈ ⋃ (i : ℕ), f '' A i constructor . -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i → y ∈ ⋃ (i : ℕ), f '' A i intro hy -- hy : y ∈ f '' ⋃ (i : ℕ), A i -- ⊢ y ∈ ⋃ (i : ℕ), f '' A i rw [mem_image] at hy -- hy : ∃ x, x ∈ ⋃ (i : ℕ), A i ∧ f x = y cases' hy with x hx -- x : α -- hx : x ∈ ⋃ (i : ℕ), A i ∧ f x = y cases' hx with xUA fxy -- xUA : x ∈ ⋃ (i : ℕ), A i -- fxy : f x = y rw [mem_iUnion] at xUA -- xUA : ∃ i, x ∈ A i cases' xUA with i xAi -- i : ℕ -- xAi : x ∈ A i rw [mem_iUnion] -- ⊢ ∃ i, y ∈ f '' A i use i -- ⊢ y ∈ f '' A i rw [←fxy] -- ⊢ f x ∈ f '' A i apply mem_image_of_mem -- ⊢ x ∈ A i exact xAi . -- ⊢ y ∈ ⋃ (i : ℕ), f '' A i → y ∈ f '' ⋃ (i : ℕ), A i intro hy -- hy : y ∈ ⋃ (i : ℕ), f '' A i -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i rw [mem_iUnion] at hy -- hy : ∃ i, y ∈ f '' A i cases' hy with i yAi -- i : ℕ -- yAi : y ∈ f '' A i cases' yAi with x hx -- x : α -- hx : x ∈ A i ∧ f x = y cases' hx with xAi fxy -- xAi : x ∈ A i -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ f '' ⋃ (i : ℕ), A i apply mem_image_of_mem -- ⊢ x ∈ ⋃ (i : ℕ), A i rw [mem_iUnion] -- ⊢ ∃ i, x ∈ A i use i -- ⊢ x ∈ A i exact xAi -- 3ª demostración -- =============== example : f '' (⋃ i, A i) = ⋃ i, f '' A i := by ext y -- y : β -- ⊢ y ∈ f '' ⋃ (i : ℕ), A i ↔ y ∈ ⋃ (i : ℕ), f '' A i simp -- ⊢ (∃ x, (∃ i, x ∈ A i) ∧ f x = y) ↔ ∃ i x, x ∈ A i ∧ f x = y constructor . -- ⊢ (∃ x, (∃ i, x ∈ A i) ∧ f x = y) → ∃ i x, x ∈ A i ∧ f x = y rintro ⟨x, ⟨i, xAi⟩, fxy⟩ -- x : α -- fxy : f x = y -- i : ℕ -- xAi : x ∈ A i -- ⊢ ∃ i x, x ∈ A i ∧ f x = y use i, x, xAi -- ⊢ f x = y exact fxy . -- ⊢ (∃ i x, x ∈ A i ∧ f x = y) → ∃ x, (∃ i, x ∈ A i) ∧ f x = y rintro ⟨i, x, xAi, fxy⟩ -- i : ℕ -- x : α -- xAi : x ∈ A i -- fxy : f x = y -- ⊢ ∃ x, (∃ i, x ∈ A i) ∧ f x = y exact ⟨x, ⟨i, xAi⟩, fxy⟩ -- 4ª demostración -- =============== example : f '' (⋃ i, A i) = ⋃ i, f '' A i := image_iUnion -- Lemas usados -- ============ -- variable (x : α) -- variable (y : β) -- variable (s : Set α) -- variable (i : ℕ) -- #check (image_iUnion : f '' ⋃ i, A i = ⋃ i, f '' A i) -- #check (mem_iUnion : x ∈ ⋃ i, A i ↔ ∃ i, x ∈ A i) -- #check (mem_iUnion_of_mem i : x ∈ A i → x ∈ ⋃ i, A i) -- #check (mem_image f s y : (y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y)) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
4.3. Demostraciones 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 |
theory Imagen_de_la_union_general imports Main begin (* 1ª demostración *) lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)" proof (rule equalityI) show "f ` (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. f ` A i)" proof (rule subsetI) fix y assume "y ∈ f ` (⋃ i ∈ I. A i)" then show "y ∈ (⋃ i ∈ I. f ` A i)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ (⋃ i ∈ I. A i)" then have "f x ∈ (⋃ i ∈ I. f ` A i)" proof (rule UN_E) fix i assume "i ∈ I" assume "x ∈ A i" then have "f x ∈ f ` A i" by (rule imageI) with ‹i ∈ I› show "f x ∈ (⋃ i ∈ I. f ` A i)" by (rule UN_I) qed with ‹y = f x› show "y ∈ (⋃ i ∈ I. f ` A i)" by (rule ssubst) qed qed next show "(⋃ i ∈ I. f ` A i) ⊆ f ` (⋃ i ∈ I. A i)" proof (rule subsetI) fix y assume "y ∈ (⋃ i ∈ I. f ` A i)" then show "y ∈ f ` (⋃ i ∈ I. A i)" proof (rule UN_E) fix i assume "i ∈ I" assume "y ∈ f ` A i" then show "y ∈ f ` (⋃ i ∈ I. A i)" proof (rule imageE) fix x assume "y = f x" assume "x ∈ A i" with ‹i ∈ I› have "x ∈ (⋃ i ∈ I. A i)" by (rule UN_I) then have "f x ∈ f ` (⋃ i ∈ I. A i)" by (rule imageI) with ‹y = f x› show "y ∈ f ` (⋃ i ∈ I. A i)" by (rule ssubst) qed qed qed qed (* 2ª demostración *) lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)" proof show "f ` (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. f ` A i)" proof fix y assume "y ∈ f ` (⋃ i ∈ I. A i)" then show "y ∈ (⋃ i ∈ I. f ` A i)" proof fix x assume "y = f x" assume "x ∈ (⋃ i ∈ I. A i)" then have "f x ∈ (⋃ i ∈ I. f ` A i)" proof fix i assume "i ∈ I" assume "x ∈ A i" then have "f x ∈ f ` A i" by simp with ‹i ∈ I› show "f x ∈ (⋃ i ∈ I. f ` A i)" by (rule UN_I) qed with ‹y = f x› show "y ∈ (⋃ i ∈ I. f ` A i)" by simp qed qed next show "(⋃ i ∈ I. f ` A i) ⊆ f ` (⋃ i ∈ I. A i)" proof fix y assume "y ∈ (⋃ i ∈ I. f ` A i)" then show "y ∈ f ` (⋃ i ∈ I. A i)" proof fix i assume "i ∈ I" assume "y ∈ f ` A i" then show "y ∈ f ` (⋃ i ∈ I. A i)" proof fix x assume "y = f x" assume "x ∈ A i" with ‹i ∈ I› have "x ∈ (⋃ i ∈ I. A i)" by (rule UN_I) then have "f x ∈ f ` (⋃ i ∈ I. A i)" by simp with ‹y = f x› show "y ∈ f ` (⋃ i ∈ I. A i)" by simp qed qed qed qed (* 3ª demostración *) lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)" by (simp only: image_UN) (* 4ª demostración *) lemma "f ` (⋃ i ∈ I. A i) = (⋃ i ∈ I. f ` A i)" by auto end |
5. Imagen de la intersección general
Demostrar con Lean4 que
\[ f\left[\bigcap_{i ∈ I} A_i\right] ⊆ \bigcap_{i ∈ I} f[A_i] \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (A : I → Set α) example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by sorry |
5.1. Demostración en lenguaje natural
Sea \(y\) tal que
\[ y ∈ f\left[\bigcap_{i ∈ I} Aᵢ\right] \tag{1} \]
Tenemos que demostrar que
\[ y ∈ \bigcap_{i ∈ I} f[Aᵢ] \]
Para ello, sea \(i ∈ I\), tenemos que demostrar que \(y ∈ f[Aᵢ]\).
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ \bigcap_{i ∈ I} Aᵢ \tag{2} \\
&f(x) = y \tag{3}
\end{align}
Por (2),
\[ x ∈ Aᵢ \]
y, por tanto,
\[ f(x) ∈ f[Aᵢ] \]
que, junto con (3), da que
\[ y ∈ f[Aᵢ] \]
5.2. Demostraciones con Lean4
|
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 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic open Set variable {α β I : Type _} variable (f : α → β) variable (A : I → Set α) -- 1ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intros y h -- y : β -- h : y ∈ f '' ⋂ (i : I), A i -- ⊢ y ∈ ⋂ (i : I), f '' A i have h1 : ∃ x, x ∈ ⋂ i, A i ∧ f x = y := (mem_image f (⋂ i, A i) y).mp h obtain ⟨x, hx : x ∈ ⋂ i, A i ∧ f x = y⟩ := h1 have h2 : x ∈ ⋂ i, A i := hx.1 have h3 : f x = y := hx.2 have h4 : ∀ i, y ∈ f '' A i := by intro i have h4a : x ∈ A i := mem_iInter.mp h2 i have h4b : f x ∈ f '' A i := mem_image_of_mem f h4a show y ∈ f '' A i rwa [h3] at h4b show y ∈ ⋂ i, f '' A i exact mem_iInter.mpr h4 -- 1ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intros y h -- y : β -- h : y ∈ f '' ⋂ (i : I), A i -- ⊢ y ∈ ⋂ (i : I), f '' A i apply mem_iInter_of_mem -- ⊢ ∀ (i : I), y ∈ f '' A i intro i -- i : I -- ⊢ y ∈ f '' A i cases' h with x hx -- x : α -- hx : x ∈ ⋂ (i : I), A i ∧ f x = y cases' hx with xIA fxy -- xIA : x ∈ ⋂ (i : I), A i -- fxy : f x = y rw [←fxy] -- ⊢ f x ∈ f '' A i apply mem_image_of_mem -- ⊢ x ∈ A i exact mem_iInter.mp xIA i -- 2ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intros y h -- y : β -- h : y ∈ f '' ⋂ (i : I), A i -- ⊢ y ∈ ⋂ (i : I), f '' A i apply mem_iInter_of_mem -- ⊢ ∀ (i : I), y ∈ f '' A i intro i -- i : I -- ⊢ y ∈ f '' A i rcases h with ⟨x, xIA, rfl⟩ -- x : α -- xIA : x ∈ ⋂ (i : I), A i -- ⊢ f x ∈ f '' A i exact mem_image_of_mem f (mem_iInter.mp xIA i) -- 3ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := by intro y -- y : β -- ⊢ y ∈ f '' ⋂ (i : I), A i → y ∈ ⋂ (i : I), f '' A i simp -- ⊢ ∀ (x : α), (∀ (i : I), x ∈ A i) → f x = y → ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y intros x xIA fxy i -- x : α -- xIA : ∀ (i : I), x ∈ A i -- fxy : f x = y -- i : I -- ⊢ ∃ x, x ∈ A i ∧ f x = y use x, xIA i -- ⊢ f x = y exact fxy -- 4ª demostración -- =============== example : f '' (⋂ i, A i) ⊆ ⋂ i, f '' A i := image_iInter_subset A f -- Lemas usados -- ============ -- variable (x : α) -- variable (s : Set α) -- #check (image_iInter_subset A f : f '' ⋂ i, A i ⊆ ⋂ i, f '' A i) -- #check (mem_iInter : x ∈ ⋂ i, A i ↔ ∀ i, x ∈ A i) -- #check (mem_iInter_of_mem : (∀ i, x ∈ A i) → x ∈ ⋂ i, A i) -- #check (mem_image_of_mem f : x ∈ s → f x ∈ f '' s) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
5.3. Demostraciones 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 |
theory Imagen_de_la_interseccion_general imports Main begin (* 1ª demostración *) lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)" proof (rule subsetI) fix y assume "y ∈ f ` (⋂ i ∈ I. A i)" then show "y ∈ (⋂ i ∈ I. f ` A i)" proof (rule imageE) fix x assume "y = f x" assume xIA : "x ∈ (⋂ i ∈ I. A i)" have "f x ∈ (⋂ i ∈ I. f ` A i)" proof (rule INT_I) fix i assume "i ∈ I" with xIA have "x ∈ A i" by (rule INT_D) then show "f x ∈ f ` A i" by (rule imageI) qed with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by (rule ssubst) qed qed (* 2ª demostración *) lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)" proof fix y assume "y ∈ f ` (⋂ i ∈ I. A i)" then show "y ∈ (⋂ i ∈ I. f ` A i)" proof fix x assume "y = f x" assume xIA : "x ∈ (⋂ i ∈ I. A i)" have "f x ∈ (⋂ i ∈ I. f ` A i)" proof fix i assume "i ∈ I" with xIA have "x ∈ A i" by simp then show "f x ∈ f ` A i" by simp qed with ‹y = f x› show "y ∈ (⋂ i ∈ I. f ` A i)" by simp qed qed (* 3ª demostración *) lemma "f ` (⋂ i ∈ I. A i) ⊆ (⋂ i ∈ I. f ` A i)" by blast end |