2ª diferencia de diferencia de conjuntos
Demostrar que
s \ (t ∪ u) ⊆ (s \ t) \ u
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : s \ (t ∪ u) ⊆ (s \ 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 71 72 73 74 75 |
import data.set.basic open set variable {α : Type} variables s t u : set α -- 1ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := begin intros x hx, split, { split, { exact hx.1, }, { dsimp, intro xt, apply hx.2, left, exact xt, }}, { dsimp, intro xu, apply hx.2, right, exact xu, }, end -- 2ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := begin rintros x ⟨xs, xntu⟩, split, { split, { exact xs, }, { intro xt, exact xntu (or.inl xt), }}, { intro xu, exact xntu (or.inr xu), }, end -- 3ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := begin rintros x ⟨xs, xntu⟩, use xs, { intro xt, exact xntu (or.inl xt) }, { intro xu, exact xntu (or.inr xu) }, end -- 4ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := begin rintros x ⟨xs, xntu⟩; finish, end -- 5ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by intro ; finish -- 6ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by rw diff_diff |
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 |
theory Diferencia_de_diferencia_de_conjuntos_2 imports Main begin (* 1ª demostración *) lemma "s - (t ∪ u) ⊆ (s - t) - u" proof (rule subsetI) fix x assume "x ∈ s - (t ∪ u)" then show "x ∈ (s - t) - u" proof (rule DiffE) assume "x ∈ s" assume "x ∉ t ∪ u" have "x ∉ u" proof (rule notI) assume "x ∈ u" then have "x ∈ t ∪ u" by (simp only: UnI2) with ‹x ∉ t ∪ u› show False by (rule notE) qed have "x ∉ t" proof (rule notI) assume "x ∈ t" then have "x ∈ t ∪ u" by (simp only: UnI1) with ‹x ∉ t ∪ u› show False by (rule notE) qed with ‹x ∈ s› have "x ∈ s - t" by (rule DiffI) then show "x ∈ (s - t) - u" using ‹x ∉ u› by (rule DiffI) qed qed (* 2ª demostración *) lemma "s - (t ∪ u) ⊆ (s - t) - u" proof fix x assume "x ∈ s - (t ∪ u)" then show "x ∈ (s - t) - u" proof assume "x ∈ s" assume "x ∉ t ∪ u" have "x ∉ u" proof assume "x ∈ u" then have "x ∈ t ∪ u" by simp with ‹x ∉ t ∪ u› show False by simp qed have "x ∉ t" proof assume "x ∈ t" then have "x ∈ t ∪ u" by simp with ‹x ∉ t ∪ u› show False by simp qed with ‹x ∈ s› have "x ∈ s - t" by simp then show "x ∈ (s - t) - u" using ‹x ∉ u› by simp qed qed (* 3ª demostración *) lemma "s - (t ∪ u) ⊆ (s - t) - u" proof fix x assume "x ∈ s - (t ∪ u)" then show "x ∈ (s - t) - u" proof assume "x ∈ s" assume "x ∉ t ∪ u" then have "x ∉ u" by simp have "x ∉ t" using ‹x ∉ t ∪ u› by simp with ‹x ∈ s› have "x ∈ s - t" by simp then show "x ∈ (s - t) - u" using ‹x ∉ u› by simp qed qed (* 4ª demostración *) lemma "s - (t ∪ u) ⊆ (s - t) - u" proof fix x assume "x ∈ s - (t ∪ u)" then show "x ∈ (s - t) - u" proof assume "x ∈ s" assume "x ∉ t ∪ u" then show "x ∈ (s - t) - u" using ‹x ∈ s› by simp qed qed (* 5ª demostración *) lemma "s - (t ∪ u) ⊆ (s - t) - u" proof fix x assume "x ∈ s - (t ∪ u)" then show "x ∈ (s - t) - u" by simp qed (* 6ª demostración *) lemma "s - (t ∪ u) ⊆ (s - t) - u" by auto end |