Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]
Demostrar con Lean4 que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[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 (u v : Set β) example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by sorry |
1. Demostración en lenguaje natural
Por la siguiente cadena de implicaciones:
\begin{align}
x ∈ f⁻¹[u] &⟹ f(x) ∈ u \\
&⟹ f(x) ∈ v &&\text{[porque \(u ⊆ v\)]} \\
&⟹ x ∈ 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 |
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (u v : Set β) -- 1ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v have h1 : f x ∈ u := mem_preimage.mp hx have h2 : f x ∈ v := h h1 show x ∈ f ⁻¹' v exact mem_preimage.mpr h2 -- 2ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v apply mem_preimage.mpr -- ⊢ f x ∈ v apply h -- ⊢ f x ∈ u apply mem_preimage.mp -- ⊢ x ∈ f ⁻¹' u exact hx -- 3ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v apply h -- ⊢ f x ∈ u exact hx -- 4ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intros x hx -- x : α -- hx : x ∈ f ⁻¹' u -- ⊢ x ∈ f ⁻¹' v exact h hx -- 5ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := fun _ hx ↦ h hx -- 6ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intro x; apply h -- 7ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := preimage_mono h -- 8ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by tauto -- Lemas usados -- ============ -- variable (a : α) -- #check (mem_preimage : a ∈ f ⁻¹' u ↔ f a ∈ u) -- #check (preimage_mono : 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 |
theory Monotonia_de_la_imagen_inversa imports Main begin (* 1ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" proof (rule subsetI) fix x assume "x ∈ f -` u" then have "f x ∈ u" by (rule vimageD) then have "f x ∈ v" using ‹u ⊆ v› by (rule set_rev_mp) then show "x ∈ f -` v" by (simp only: vimage_eq) qed (* 2ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" proof fix x assume "x ∈ f -` u" then have "f x ∈ u" by simp then have "f x ∈ v" using ‹u ⊆ v› by (rule set_rev_mp) then show "x ∈ f -` v" by simp qed (* 3ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" using assms by (simp only: vimage_mono) (* 4ª demostración *) lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" using assms by blast end |
