Imagen inversa de la intersección
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 que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 |
import data.set.basic open set variables {α : Type*} {β : Type*} variable f : α → β variables u v : set β example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := 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 |
import data.set.basic open set variables {α : Type*} {β : Type*} variable f : α → β variables u v : set β -- 1ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := begin ext x, split, { intro h, split, { apply mem_preimage.mpr, rw mem_preimage at h, exact mem_of_mem_inter_left h, }, { apply mem_preimage.mpr, rw mem_preimage at h, exact mem_of_mem_inter_right h, }}, { intro h, apply mem_preimage.mpr, split, { apply mem_preimage.mp, exact mem_of_mem_inter_left h,}, { apply mem_preimage.mp, exact mem_of_mem_inter_right h, }}, end -- 2ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := begin ext x, split, { intro h, split, { simp at *, exact h.1, }, { simp at *, exact h.2, }}, { intro h, simp at *, exact h, }, end -- 3ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := -- by hint by finish -- 4ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := -- by library_search preimage_inter -- 5ª demostración -- =============== example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := rfl |
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 142 143 144 145 146 147 148 149 150 151 |
theory Imagen_inversa_de_la_interseccion imports Main begin section ‹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 section ‹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 section ‹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 section ‹4ª demostración› lemma "f -` (u ∩ v) = f -` u ∩ f -` v" by (simp only: vimage_Int) section ‹5ª demostración› lemma "f -` (u ∩ v) = f -` u ∩ f -` v" by auto end |