Conmutatividad de la intersección
Demostrar que
s ∩ t = 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 u : set α example : s ∩ t = t ∩ s := sorry |
Notas
- En este enlace se puede escribir las soluciones en Lean.
- A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
- En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>
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 |
import data.set.basic open set variable {α : Type} variables s t u : set α -- 1ª demostración -- =============== example : s ∩ t = t ∩ s := begin ext x, simp only [mem_inter_eq], split, { intro h, split, { exact h.2, }, { exact h.1, }}, { intro h, split, { exact h.2, }, { exact h.1, }}, end -- 2ª demostración -- =============== example : s ∩ t = t ∩ s := begin ext, simp only [mem_inter_eq], exact ⟨λ h, ⟨h.2, h.1⟩, λ h, ⟨h.2, h.1⟩⟩, end -- 3ª demostración -- =============== example : s ∩ t = t ∩ s := begin ext, exact ⟨λ h, ⟨h.2, h.1⟩, λ h, ⟨h.2, h.1⟩⟩, end -- 4ª demostración -- =============== example : s ∩ t = t ∩ s := begin ext x, simp only [mem_inter_eq], split, { rintros ⟨xs, xt⟩, exact ⟨xt, xs⟩ }, { rintros ⟨xt, xs⟩, exact ⟨xs, xt⟩ }, end -- 5ª demostración -- =============== example : s ∩ t = t ∩ s := begin ext x, exact and.comm, end -- 6ª demostración -- =============== example : s ∩ t = t ∩ s := ext (λ x, and.comm) -- 7ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x; simp [and.comm] -- 8ª demostración -- =============== example : s ∩ t = t ∩ s := inter_comm s t -- 9ª demostración -- =============== example : s ∩ t = t ∩ s := by finish |
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 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 |
theory Conmutatividad_de_la_interseccion imports Main begin (* 1ª demostración *) lemma "s ∩ t = t ∩ s" proof (rule set_eqI) fix x show "x ∈ s ∩ t ⟷ x ∈ t ∩ s" proof (rule iffI) assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ t" using h by (simp only: IntD2) then show "x ∈ t ∩ s" using xs by (rule IntI) next assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by (simp only: IntD1) have xs : "x ∈ s" using h by (simp only: IntD2) then show "x ∈ s ∩ t" using xt by (rule IntI) qed qed (* 2ª demostración *) lemma "s ∩ t = t ∩ s" proof (rule set_eqI) fix x show "x ∈ s ∩ t ⟷ x ∈ t ∩ s" proof assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by simp have xt : "x ∈ t" using h by simp then show "x ∈ t ∩ s" using xs by simp next assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by simp have xs : "x ∈ s" using h by simp then show "x ∈ s ∩ t" using xt by simp qed qed (* 3ª demostración *) lemma "s ∩ t = t ∩ s" proof (rule equalityI) show "s ∩ t ⊆ t ∩ s" proof (rule subsetI) fix x assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ t" using h by (simp only: IntD2) then show "x ∈ t ∩ s" using xs by (rule IntI) qed next show "t ∩ s ⊆ s ∩ t" proof (rule subsetI) fix x assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by (simp only: IntD1) have xs : "x ∈ s" using h by (simp only: IntD2) then show "x ∈ s ∩ t" using xt by (rule IntI) qed qed (* 4ª demostración *) lemma "s ∩ t = t ∩ s" proof show "s ∩ t ⊆ t ∩ s" proof fix x assume h : "x ∈ s ∩ t" then have xs : "x ∈ s" by simp have xt : "x ∈ t" using h by simp then show "x ∈ t ∩ s" using xs by simp qed next show "t ∩ s ⊆ s ∩ t" proof fix x assume h : "x ∈ t ∩ s" then have xt : "x ∈ t" by simp have xs : "x ∈ s" using h by simp then show "x ∈ s ∩ t" using xt by simp qed qed (* 5ª demostración *) lemma "s ∩ t = t ∩ s" proof show "s ∩ t ⊆ t ∩ s" proof fix x assume "x ∈ s ∩ t" then show "x ∈ t ∩ s" by simp qed next show "t ∩ s ⊆ s ∩ t" proof fix x assume "x ∈ t ∩ s" then show "x ∈ s ∩ t" by simp qed qed (* 6ª demostración *) lemma "s ∩ t = t ∩ s" by (fact Int_commute) (* 7ª demostración *) lemma "s ∩ t = t ∩ s" by (fact inf_commute) (* 8ª demostración *) lemma "s ∩ t = t ∩ s" by auto end |