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 |
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}
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. 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 |
