f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]
En Lean, la imagen inversa de un conjunto s
(de elementos de tipo β
) por la función f
(de tipo α → β
) es el conjunto f ⁻¹' s
de elementos x
(de tipo α
) tales que f x ∈ s
.
Demostrar con Lean4 que
1 |
f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v |
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Set.Function variable {α β : Type _} variable (f : α → β) variable (u v : Set β) open Set example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que, para todo \(x\),
\[ x ∈ f⁻¹[u ∩ v] ↔ x ∈ f⁻¹[u] ∩ f⁻¹[v] \]
Lo haremos mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ f⁻¹[u ∩ v] &↔ f x ∈ u ∩ v \\
&↔ f x ∈ u ∧ f x ∈ v \\
&↔ x ∈ f⁻¹[u] ∧ x ∈ f⁻¹[v] \\
&↔ x ∈ f⁻¹[u] ∩ f⁻¹[v] \\
\end{align}
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 |
import Mathlib.Data.Set.Function variable {α β : Type _} variable (f : α → β) variable (u v : Set β) open Set -- 1ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (u ∩ v) ↔ x ∈ f ⁻¹' u ∩ f ⁻¹' v calc x ∈ f ⁻¹' (u ∩ v) ↔ f x ∈ u ∩ v := by simp only [mem_preimage] _ ↔ f x ∈ u ∧ f x ∈ v := by simp only [mem_inter_iff] _ ↔ x ∈ f ⁻¹' u ∧ x ∈ f ⁻¹' v := by simp only [mem_preimage] _ ↔ x ∈ f ⁻¹' u ∩ f ⁻¹' v := by simp only [mem_inter_iff] -- 2ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (u ∩ v) ↔ x ∈ f ⁻¹' u ∩ f ⁻¹' v constructor . -- ⊢ x ∈ f ⁻¹' (u ∩ v) → x ∈ f ⁻¹' u ∩ f ⁻¹' v intro h -- h : x ∈ f ⁻¹' (u ∩ v) -- ⊢ x ∈ f ⁻¹' u ∩ f ⁻¹' v constructor . -- ⊢ x ∈ f ⁻¹' u apply mem_preimage.mpr -- ⊢ f x ∈ u rw [mem_preimage] at h -- h : f x ∈ u ∩ v exact mem_of_mem_inter_left h . -- ⊢ x ∈ f ⁻¹' v apply mem_preimage.mpr -- ⊢ f x ∈ v rw [mem_preimage] at h -- h : f x ∈ u ∩ v exact mem_of_mem_inter_right h . -- ⊢ x ∈ f ⁻¹' u ∩ f ⁻¹' v → x ∈ f ⁻¹' (u ∩ v) intro h -- h : x ∈ f ⁻¹' u ∩ f ⁻¹' v -- ⊢ x ∈ f ⁻¹' (u ∩ v) apply mem_preimage.mpr -- ⊢ f x ∈ u ∩ v constructor . -- ⊢ f x ∈ u apply mem_preimage.mp -- ⊢ x ∈ f ⁻¹' u exact mem_of_mem_inter_left h . -- ⊢ f x ∈ v apply mem_preimage.mp -- ⊢ x ∈ f ⁻¹' v exact mem_of_mem_inter_right h -- 3ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by ext x -- x : α -- ⊢ x ∈ f ⁻¹' (u ∩ v) ↔ x ∈ f ⁻¹' u ∩ f ⁻¹' v constructor . -- ⊢ x ∈ f ⁻¹' (u ∩ v) → x ∈ f ⁻¹' u ∩ f ⁻¹' v intro h -- h : x ∈ f ⁻¹' (u ∩ v) -- ⊢ x ∈ f ⁻¹' u ∩ f ⁻¹' v constructor . -- ⊢ x ∈ f ⁻¹' u simp at * -- h : f x ∈ u ∧ f x ∈ v -- ⊢ f x ∈ u exact h.1 . -- ⊢ x ∈ f ⁻¹' v simp at * -- h : f x ∈ u ∧ f x ∈ v -- ⊢ f x ∈ v exact h.2 . -- ⊢ x ∈ f ⁻¹' u ∩ f ⁻¹' v → x ∈ f ⁻¹' (u ∩ v) intro h -- h : x ∈ f ⁻¹' u ∩ f ⁻¹' v -- ⊢ x ∈ f ⁻¹' (u ∩ v) simp at * -- h : f x ∈ u ∧ f x ∈ v -- ⊢ f x ∈ u ∧ f x ∈ v exact h -- 4ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by aesop -- 5ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := preimage_inter -- 6ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := rfl -- Lemas usados -- ============ -- variable (x : α) -- variable (s t : Set α) -- #check (mem_of_mem_inter_left : x ∈ s ∩ t → x ∈ s) -- #check (mem_of_mem_inter_right : x ∈ s ∩ t → x ∈ t) -- #check (mem_preimage : x ∈ f ⁻¹' u ↔ f x ∈ u) -- #check (preimage_inter : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v) |
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 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 |
theory Imagen_inversa_de_la_interseccion imports Main begin (* 1ª demostración *) lemma "f -` (u ∩ v) = f -` u ∩ f -` v" proof (rule equalityI) show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v" proof (rule subsetI) fix x assume "x ∈ f -` (u ∩ v)" then have h : "f x ∈ u ∩ v" by (simp only: vimage_eq) have "x ∈ f -` u" proof - have "f x ∈ u" using h by (rule IntD1) then show "x ∈ f -` u" by (rule vimageI2) qed moreover have "x ∈ f -` v" proof - have "f x ∈ v" using h by (rule IntD2) then show "x ∈ f -` v" by (rule vimageI2) qed ultimately show "x ∈ f -` u ∩ f -` v" by (rule IntI) qed next show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)" proof (rule subsetI) fix x assume h2 : "x ∈ f -` u ∩ f -` v" have "f x ∈ u" proof - have "x ∈ f -` u" using h2 by (rule IntD1) then show "f x ∈ u" by (rule vimageD) qed moreover have "f x ∈ v" proof - have "x ∈ f -` v" using h2 by (rule IntD2) then show "f x ∈ v" by (rule vimageD) qed ultimately have "f x ∈ u ∩ v" by (rule IntI) then show "x ∈ f -` (u ∩ v)" by (rule vimageI2) qed qed (* 2ª demostración *) lemma "f -` (u ∩ v) = f -` u ∩ f -` v" proof show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v" proof fix x assume "x ∈ f -` (u ∩ v)" then have h : "f x ∈ u ∩ v" by simp have "x ∈ f -` u" proof - have "f x ∈ u" using h by simp then show "x ∈ f -` u" by simp qed moreover have "x ∈ f -` v" proof - have "f x ∈ v" using h by simp then show "x ∈ f -` v" by simp qed ultimately show "x ∈ f -` u ∩ f -` v" by simp qed next show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)" proof fix x assume h2 : "x ∈ f -` u ∩ f -` v" have "f x ∈ u" proof - have "x ∈ f -` u" using h2 by simp then show "f x ∈ u" by simp qed moreover have "f x ∈ v" proof - have "x ∈ f -` v" using h2 by simp then show "f x ∈ v" by simp qed ultimately have "f x ∈ u ∩ v" by simp then show "x ∈ f -` (u ∩ v)" by simp qed qed (* 3ª demostración *) lemma "f -` (u ∩ v) = f -` u ∩ f -` v" proof show "f -` (u ∩ v) ⊆ f -` u ∩ f -` v" proof fix x assume h1 : "x ∈ f -` (u ∩ v)" have "x ∈ f -` u" using h1 by simp moreover have "x ∈ f -` v" using h1 by simp ultimately show "x ∈ f -` u ∩ f -` v" by simp qed next show "f -` u ∩ f -` v ⊆ f -` (u ∩ v)" proof fix x assume h2 : "x ∈ f -` u ∩ f -` v" have "f x ∈ u" using h2 by simp moreover have "f x ∈ v" using h2 by simp ultimately have "f x ∈ u ∩ v" by simp then show "x ∈ f -` (u ∩ v)" by simp qed qed (* 4ª demostración *) lemma "f -` (u ∩ v) = f -` u ∩ f -` v" by (simp only: vimage_Int) (* 5ª demostración *) lemma "f -` (u ∩ v) = f -` u ∩ f -` v" by auto end |