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 8 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic 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\).
(⟸) 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 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 133 134 135 136 137 138 139 140 141 142 |
import Mathlib.Data.Set.Basic import Mathlib.Tactic 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 intros h -- h : x ∈ s ∩ (s ∪ t) -- ⊢ x ∈ s exact h.1 . -- ⊢ x ∈ s → x ∈ s ∩ (s ∪ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ 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 constructor . -- ⊢ x ∈ s ∩ (s ∪ t) → x ∈ s intro h -- h : x ∈ s ∩ (s ∪ t) -- ⊢ x ∈ s exact h.1 . -- ⊢ x ∈ s → x ∈ s ∩ (s ∪ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s ∪ t exact (Or.inl xs) -- 3ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s exact ⟨fun h ↦ h.1, fun xs ↦ ⟨xs, Or.inl xs⟩⟩ -- 4ª demostración -- =============== example : s ∩ (s ∪ t) = s := by ext -- x : α -- ⊢ x ∈ s ∩ (s ∪ t) ↔ x ∈ s exact ⟨And.left, fun xs ↦ ⟨xs, Or.inl xs⟩⟩ -- 5ª 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 : x ∈ s -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ s → x ∈ s ∩ (s ∪ t) intro xs -- xs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) use xs -- ⊢ x ∈ s ∪ t left -- ⊢ x ∈ s exact xs -- 6ª demostración -- =============== example : s ∩ (s ∪ t) = s := by apply subset_antisymm . -- ⊢ s ∩ (s ∪ t) ⊆ s rintro x ⟨hxs, -⟩ -- x : α -- hxs : x ∈ s -- ⊢ x ∈ s exact hxs . -- ⊢ s ⊆ s ∩ (s ∪ t) intros x hxs -- x : α -- hxs : x ∈ s -- ⊢ x ∈ s ∩ (s ∪ t) exact ⟨hxs, Or.inl hxs⟩ -- 7ª demostración -- =============== example : s ∩ (s ∪ t) = s := inf_sup_self -- 8ª demostración -- =============== example : s ∩ (s ∪ t) = s := by aesop -- Lemas usados -- ============ -- variable (a b : Prop) -- #check (And.left : a ∧ b → a) -- #check (Or.inl : a → a ∨ b) -- #check (inf_sup_self : s ∩ (s ∪ t) = s) -- #check (subset_antisymm : s ⊆ t → t ⊆ s → s = t) |
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 |
theory Interseccion_con_su_union 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" by (simp only: IntD1) qed next show "s ⊆ s ∩ (s ∪ t)" proof (rule subsetI) fix x assume "x ∈ s" then have "x ∈ s ∪ t" by (simp only: UnI1) with ‹x ∈ s› show "x ∈ s ∩ (s ∪ t)" by (rule IntI) 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" by simp qed next show "s ⊆ s ∩ (s ∪ t)" proof fix x assume "x ∈ s" then have "x ∈ s ∪ t" by simp then show "x ∈ s ∩ (s ∪ t)" using ‹x ∈ s› by simp qed qed (* 3ª demostración *) lemma "s ∩ (s ∪ t) = s" by (fact Un_Int_eq) (* 4ª demostración *) lemma "s ∩ (s ∪ t) = s" by auto |
