Propiedad de monotonía de la intersección
Demostrar que la intersección es monótona por la izquierda; es decir, si
s ⊆ t,
entonces
s ∩ u ⊆ t ∩ u.
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 variable {α : Type} variables s t u : set α example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := sorry |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
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 |
import data.set.basic open set variable {α : Type} variables s t u : set α -- 1ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin rw subset_def, rw inter_def, rw inter_def, dsimp, intros x h, cases h with xs xu, split, { rw subset_def at h, apply h, assumption }, { assumption }, end -- 2ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin rw [subset_def, inter_def, inter_def], dsimp, rintros x ⟨xs, xu⟩, rw subset_def at h, exact ⟨h _ xs, xu⟩, end -- 3ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin simp only [subset_def, mem_inter_eq] at *, rintros x ⟨xs, xu⟩, exact ⟨h _ xs, xu⟩, end -- 4ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := begin intros x xsu, exact ⟨h xsu.1, xsu.2⟩, end -- 5ª demostración -- =============== example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := inter_subset_inter_left u h |
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 |
theory Propiedad_de_monotonia_de_la_interseccion imports Main begin (* 1ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof (rule subsetI) fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by (simp only: IntD1) then have xt: "x ∈ t" using assms by (simp only: subset_eq) have xu: "x ∈ u" using hx by (simp only: IntD2) show "x ∈ t ∩ u" using xt xu by (simp only: Int_iff) qed (* 2 solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" proof fix x assume hx: "x ∈ s ∩ u" have xs: "x ∈ s" using hx by simp then have xt: "x ∈ t" using assms by auto have xu: "x ∈ u" using hx by simp show "x ∈ t ∩ u" using xt xu by simp qed (* 3ª solución *) lemma assumes "s ⊆ t" shows "s ∩ u ⊆ t ∩ u" using assms by auto (* 4ª solución *) lemma "s ⊆ t ⟹ s ∩ u ⊆ t ∩ u" by auto end |
