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 |
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ᵢ] \]
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.
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 |
