Monotonía de la imagen inversa
Demostrar que si u ⊆ v, entonces
|
1 |
f⁻¹[u] ⊆ f⁻¹[v] |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.set.basic open set variables {α : Type*} {β : Type*} variable f : α → β variables u v : set β example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := sorry |
[expand title=»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 70 71 72 73 74 75 |
import data.set.basic open set variables {α : Type*} {β : Type*} variable f : α → β variables u v : set β -- 1ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := begin intros x hx, apply mem_preimage.mpr, apply h, apply mem_preimage.mp, exact hx, end -- 2ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := begin intros x hx, apply h, exact hx, end -- 3ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := begin intros x hx, exact h hx, end -- 4ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := λ x hx, h hx -- 5ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by intro x; apply h -- 6ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := preimage_mono h -- 7ª demostración -- =============== example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by tauto |
Se puede interactuar con la prueba anterior en esta sesión con Lean,
[/expand]
[expand title=»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 |
theory Monotonia_de_la_imagen_inversa imports Main begin section ‹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 section ‹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 section ‹3ª demostración› lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" using assms by (simp only: vimage_mono) section ‹4ª demostración› lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" using assms by blast end |
[/expand]
[expand title=»Nuevas soluciones»]
- En los comentarios se pueden escribir nuevas soluciones.
- El código se debe escribir entre una línea con <pre lang="lean"> (o <pre lang="isar">) y otra con </pre>
[/expand]