(s \ t) \ u ⊆ s \ (t ∪ u)
Demostrar con Lean4 que
\[ (s \setminus t) \setminus u ⊆ s \setminus (t ∪ u) \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) example : (s \ t) \ u ⊆ s \ (t ∪ u) := by sorry |
1. Demostración en lenguaje natural
Sea \(x ∈ (s \setminus t) \setminus u\). Entonces, se tiene que
\begin{align}
&x ∈ s \tag{1} \\
&x ∉ t \tag{2} \\
&x ∉ u \tag{3}
\end{align}
Tenemos que demostrar que
\[ x ∈ s \setminus (t ∪ u) \]
pero, por (1), se reduce a
\[ x ∉ t ∪ u \]
que se verifica por (2) y (3).
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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) -- 1ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by intros x hx -- x : α -- hx : x ∈ (s \ t) \ u -- ⊢ x ∈ s \ (t ∪ u) rcases hx with ⟨hxst, hxnu⟩ -- hxst : x ∈ s \ t -- hxnu : ¬x ∈ u rcases hxst with ⟨hxs, hxnt⟩ -- hxs : x ∈ s -- hxnt : ¬x ∈ t constructor . -- ⊢ x ∈ s exact hxs . -- ⊢ ¬x ∈ t ∪ u by_contra hxtu -- hxtu : x ∈ t ∪ u -- ⊢ False rcases hxtu with (hxt | hxu) . -- hxt : x ∈ t apply hxnt -- ⊢ x ∈ t exact hxt . -- hxu : x ∈ u apply hxnu -- ⊢ x ∈ u exact hxu -- 2ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rintro x ⟨⟨hxs, hxnt⟩, hxnu⟩ -- x : α -- hxnu : ¬x ∈ u -- hxs : x ∈ s -- hxnt : ¬x ∈ t -- ⊢ x ∈ s \ (t ∪ u) constructor . -- ⊢ x ∈ s exact hxs . -- ⊢ ¬x ∈ t ∪ u by_contra hxtu -- hxtu : x ∈ t ∪ u -- ⊢ False rcases hxtu with (hxt | hxu) . -- hxt : x ∈ t exact hxnt hxt . -- hxu : x ∈ u exact hxnu hxu -- 3ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rintro x ⟨⟨xs, xnt⟩, xnu⟩ -- x : α -- xnu : ¬x ∈ u -- xs : x ∈ s -- xnt : ¬x ∈ t -- ⊢ x ∈ s \ (t ∪ u) use xs -- ⊢ ¬x ∈ t ∪ u rintro (xt | xu) . -- xt : x ∈ t -- ⊢ False contradiction . -- xu : x ∈ u -- ⊢ False contradiction -- 4ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rintro x ⟨⟨xs, xnt⟩, xnu⟩ -- x : α -- xnu : ¬x ∈ u -- xs : x ∈ s -- xnt : ¬x ∈ t -- ⊢ x ∈ s \ (t ∪ u) use xs -- ⊢ ¬x ∈ t ∪ u rintro (xt | xu) <;> contradiction -- 5ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by intro x xstu -- x : α -- xstu : x ∈ (s \ t) \ u -- ⊢ x ∈ s \ (t ∪ u) simp at * -- ⊢ x ∈ s ∧ ¬(x ∈ t ∨ x ∈ u) aesop -- 6ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by intro x xstu -- x : α -- xstu : x ∈ (s \ t) \ u -- ⊢ x ∈ s \ (t ∪ u) aesop -- 7ª demostración -- =============== example : (s \ t) \ u ⊆ s \ (t ∪ u) := by rw [diff_diff] -- Lema usado -- ========== -- #check (diff_diff : (s \ t) \ u = s \ (t ∪ u)) |
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 71 |
theory Diferencia_de_diferencia_de_conjuntos imports Main begin (* 1ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" proof (rule subsetI) fix x assume hx : "x ∈ (s - t) - u" then show "x ∈ s - (t ∪ u)" proof (rule DiffE) assume xst : "x ∈ s - t" assume xnu : "x ∉ u" note xst then show "x ∈ s - (t ∪ u)" proof (rule DiffE) assume xs : "x ∈ s" assume xnt : "x ∉ t" have xntu : "x ∉ t ∪ u" proof (rule notI) assume xtu : "x ∈ t ∪ u" then show False proof (rule UnE) assume xt : "x ∈ t" with xnt show False by (rule notE) next assume xu : "x ∈ u" with xnu show False by (rule notE) qed qed show "x ∈ s - (t ∪ u)" using xs xntu by (rule DiffI) qed qed qed (* 2ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" proof fix x assume hx : "x ∈ (s - t) - u" then have xst : "x ∈ (s - t)" by simp then have xs : "x ∈ s" by simp have xnt : "x ∉ t" using xst by simp have xnu : "x ∉ u" using hx by simp have xntu : "x ∉ t ∪ u" using xnt xnu by simp then show "x ∈ s - (t ∪ u)" using xs by simp 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)" by simp qed (* 4ª demostración *) lemma "(s - t) - u ⊆ s - (t ∪ u)" by auto end |
