s \ (t ∪ u) ⊆ (s \ t) \ u
Demostrar con Lean4 que
\[ s \setminus (t ∪ u) ⊆ (s \setminus t) \setminus 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 ∪ u)\). Entonces,
\begin{align}
&x ∈ s \tag{1} \\
&x ∉ t ∪ u \tag{2} \\
\end{align}
Tenemos que demostrar que \(x ∈ (s \setminus t) \setminus u\); es decir, que se verifican las relaciones
\begin{align}
&x ∈ s \setminus t \tag{3} \\
&x ∉ u \tag{4}
\end{align}
Para demostrar (3) tenemos que demostrar las relaciones
\begin{align}
&x ∈ s \tag{5} \\
&x ∉ t \tag{6}
\end{align}
La (5) se tiene por la (1). Para demostrar la (6), supongamos que \(x ∈ t\); entonces, \(x ∈ t ∪ u\), en contracción con (2). Para demostrar la (4), supongamos que \(x ∈ u\); entonces, \(x ∈ t ∪ u\), en contracción con (2).
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 |
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 constructor . -- ⊢ x ∈ s \ t constructor . -- ⊢ x ∈ s exact hx.1 . -- ⊢ ¬x ∈ t intro xt -- xt : x ∈ t -- ⊢ False apply hx.2 -- ⊢ x ∈ t ∪ u left -- ⊢ x ∈ t exact xt . -- ⊢ ¬x ∈ u intro xu -- xu : x ∈ u -- ⊢ False apply hx.2 -- ⊢ x ∈ t ∪ u right -- ⊢ x ∈ u exact xu -- 2ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by rintro x ⟨xs, xntu⟩ -- x : α -- xs : x ∈ s -- xntu : ¬x ∈ t ∪ u -- ⊢ x ∈ (s \ t) \ u constructor . -- ⊢ x ∈ s \ t constructor . -- ⊢ x ∈ s exact xs . -- ¬x ∈ t intro xt -- xt : x ∈ t -- ⊢ False exact xntu (Or.inl xt) . -- ⊢ ¬x ∈ u intro xu -- xu : x ∈ u -- ⊢ False exact xntu (Or.inr xu) -- 2ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := fun _ ⟨xs, xntu⟩ ↦ ⟨⟨xs, fun xt ↦ xntu (Or.inl xt)⟩, fun xu ↦ xntu (Or.inr xu)⟩ -- 4ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by rintro x ⟨xs, xntu⟩ -- x : α -- xs : x ∈ s -- xntu : ¬x ∈ t ∪ u -- ⊢ x ∈ (s \ t) \ u aesop -- 5ª demostración -- =============== example : s \ (t ∪ u) ⊆ (s \ t) \ u := by intro ; aesop -- 6ª 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_2 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 |
