s ∩ t = t ∩ s
Demostrar con Lean4 que
\[ s ∩ t = 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 ∩ t = t ∩ s := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∩ t ↔ x ∈ t ∩ s] \]
Demostratemos la equivalencia por la doble implicación.
Sea \(x ∈ s ∩ t\). Entonces, se tiene
\begin{align}
&x ∈ s \tag{1} \\
&x ∈ t \tag{2}
\end{align}
Luego \(x ∈ t ∩ s\) (por (2) y (1)).
La segunda implicación se demuestra análogamente.
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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) -- 1ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s constructor . -- ⊢ x ∈ s ∧ x ∈ t → x ∈ t ∧ x ∈ s intro h -- h : x ∈ s ∧ x ∈ t -- ⊢ x ∈ t ∧ x ∈ s constructor . -- ⊢ x ∈ t exact h.2 . -- ⊢ x ∈ s exact h.1 . -- ⊢ x ∈ t ∧ x ∈ s → x ∈ s ∧ x ∈ t intro h -- h : x ∈ t ∧ x ∈ s -- ⊢ x ∈ s ∧ x ∈ t constructor . -- ⊢ x ∈ s exact h.2 . -- ⊢ x ∈ t exact h.1 -- 2ª demostración -- =============== example : s ∩ t = t ∩ s := by ext -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s exact ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩ -- 3ª demostración -- =============== example : s ∩ t = t ∩ s := by ext -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s exact ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩ -- 4ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s constructor . -- ⊢ x ∈ s ∧ x ∈ t → x ∈ t ∧ x ∈ s rintro ⟨xs, xt⟩ -- xs : x ∈ s -- xt : x ∈ t -- ⊢ x ∈ t ∧ x ∈ s exact ⟨xt, xs⟩ . -- ⊢ x ∈ t ∧ x ∈ s → x ∈ s ∧ x ∈ t rintro ⟨xt, xs⟩ -- xt : x ∈ t -- xs : x ∈ s -- ⊢ x ∈ s ∧ x ∈ t exact ⟨xs, xt⟩ -- 5ª demostración -- =============== example : s ∩ t = t ∩ s := by ext x -- x : α -- ⊢ x ∈ s ∩ t ↔ x ∈ t ∩ s simp only [mem_inter_iff] -- ⊢ x ∈ s ∧ x ∈ t ↔ x ∈ t ∧ x ∈ s simp only [And.comm] -- 6ª demostración -- =============== example : s ∩ t = t ∩ s := ext (fun _ ↦ And.comm) -- 7ª demostración -- =============== example : s ∩ t = t ∩ s := by ext ; simp [And.comm] -- 8ª demostración -- =============== example : s ∩ t = t ∩ s := inter_comm s t -- Lemas usados -- ============ -- variable (x : α) -- variable (a b : Prop) -- #check (And.comm : a ∧ b ↔ b ∧ a) -- #check (inter_comm s t : s ∩ t = t ∩ s) -- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ 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 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 |
