s ∪ (s ∩ t) = s
Demostrar con Lean4 que
\[ s ∪ (s ∩ t) = s \]
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 : Set α) example : s ∪ (s ∩ t) = s := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∪ (s ∩ t) ↔ x ∈ s] \]
y lo haremos demostrando las dos implicaciones.
(⟹) Sea \(x ∈ s ∪ (s ∩ t)\). Entonces, \(x ∈ s\) ó \(x ∈ s ∩ t\). En ambos casos, \(x ∈ s\).
(⟸) Sea \(x ∈ s\). Entonces, \(x ∈ s ∩ t\) y, por tanto, \(x ∈ s ∪ (s ∩ t)\).
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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) -- 1ª demostración -- =============== example : s ∪ (s ∩ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∪ (s ∩ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∪ (s ∩ t) → x ∈ s intro hx -- hx : x ∈ s ∪ (s ∩ t) -- ⊢ x ∈ s rcases hx with (xs | xst) . -- xs : x ∈ s exact xs . -- xst : x ∈ s ∩ t exact xst.1 . -- ⊢ x ∈ s → x ∈ s ∪ (s ∩ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∪ (s ∩ t) left -- ⊢ x ∈ s exact xs -- 2ª demostración -- =============== example : s ∪ (s ∩ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∪ s ∩ t ↔ x ∈ s exact ⟨fun hx ↦ Or.elim hx id And.left, fun xs ↦ Or.inl xs⟩ -- 3ª demostración -- =============== example : s ∪ (s ∩ t) = s := by ext x -- x : α -- ⊢ x ∈ s ∪ (s ∩ t) ↔ x ∈ s constructor . -- ⊢ x ∈ s ∪ (s ∩ t) → x ∈ s rintro (xs | ⟨xs, -⟩) <;> -- xs : x ∈ s -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s → x ∈ s ∪ (s ∩ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∪ s ∩ t left -- ⊢ x ∈ s exact xs -- 4ª demostración -- =============== example : s ∪ (s ∩ t) = s := sup_inf_self -- Lemas usados -- ============ -- variable (a b c : Prop) -- #check (And.left : a ∧ b → a) -- #check (Or.elim : a ∨ b → (a → c) → (b → c) → c) -- #check (sup_inf_self : s ∪ (s ∩ t) = s) |
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 |
theory Union_con_su_interseccion imports Main begin (* 1ª demostración *) lemma "s ∪ (s ∩ t) = s" proof (rule equalityI) show "s ∪ (s ∩ t) ⊆ s" proof (rule subsetI) fix x assume "x ∈ s ∪ (s ∩ t)" then show "x ∈ s" proof assume "x ∈ s" then show "x ∈ s" by this next assume "x ∈ s ∩ t" then show "x ∈ s" by (simp only: IntD1) qed qed next show "s ⊆ s ∪ (s ∩ t)" proof (rule subsetI) fix x assume "x ∈ s" then show "x ∈ s ∪ (s ∩ t)" by (simp only: UnI1) qed qed (* 2ª demostración *) lemma "s ∪ (s ∩ t) = s" proof show "s ∪ s ∩ t ⊆ s" proof fix x assume "x ∈ s ∪ (s ∩ t)" then show "x ∈ s" proof assume "x ∈ s" then show "x ∈ s" by this next assume "x ∈ s ∩ t" then show "x ∈ s" by simp qed qed next show "s ⊆ s ∪ (s ∩ t)" proof fix x assume "x ∈ s" then show "x ∈ s ∪ (s ∩ t)" by simp qed qed (* 3ª demostración *) lemma "s ∪ (s ∩ t) = s" by auto end |
