Intersección con su unión
Demostrar que s ∩ (s ∪ t) = s
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 : set α example : s ∩ (s ∪ t) = s := sorry |
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 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 |
import data.set.basic import tactic open set variable {α : Type} variables s t : set α -- 1ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin ext x, split, { intros h, dsimp at h, exact h.1, }, { intro xs, dsimp, split, { exact xs, }, { left, exact xs, }}, end -- 2ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin ext x, split, { intros h, exact h.1, }, { intro xs, split, { exact xs, }, { left, exact xs, }}, end -- 3ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin ext x, split, { intros h, exact h.1, }, { intro xs, split, { exact xs, }, { exact (or.inl xs), }}, end -- 4ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin ext, exact ⟨λ h, h.1, λ xs, ⟨xs, or.inl xs⟩⟩, end -- 5ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin ext, exact ⟨and.left, λ xs, ⟨xs, or.inl xs⟩⟩, end -- 6ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin ext x, split, { rintros ⟨xs, _⟩, exact xs }, { intro xs, use xs, left, exact xs }, end -- 7ª demostración -- =============== example : s ∩ (s ∪ t) = s := begin apply subset_antisymm, { rintros x ⟨hxs,-⟩, exact hxs, }, { intros x hxs, exact ⟨hxs, or.inl hxs⟩, }, end -- 8ª demostración -- =============== example : s ∩ (s ∪ t) = s := -- by suggest inf_sup_self -- 9ª demostración -- =============== example : s ∩ (s ∪ t) = s := -- by hint by finish |
El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.
La construcción de las demostraciones se muestra en el siguiente vídeo
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 |
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 |