s ∩ (⋃ᵢ Aᵢ) = ⋃ᵢ (Aᵢ ∩ s)
Demostrar con Lean4 que
\[ s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s) \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Lattice import Mathlib.Tactic open Set variable {α : Type} variable (s : Set α) variable (A : ℕ → Set α) example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by sorry |
1. Demostración en lenguaje natural
Tenemos que demostrar que para cada \(x\), se verifica que
\[ x ∈ s ∩ ⋃_i A_i ↔ x ∈ ⋃_i A_i ∩ s \]
Lo demostramos mediante la siguiente cadena de equivalencias
\begin{align}
x ∈ s ∩ ⋃_i A_i &↔ x ∈ s ∧ x ∈ ⋃_i A_i \\
&↔ x ∈ s ∧ (∃ i)[x ∈ A_i] \\
&↔ (∃ i)[x ∈ s ∧ x ∈ A_i] \\
&↔ (∃ i)[x ∈ A_i ∧ x ∈ s] \\
&↔ (∃ i)[x ∈ A_i ∩ s] \\
&↔ x ∈ ⋃_i (A i ∩ s)
\end{align}
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 |
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Lattice import Mathlib.Tactic open Set variable {α : Type} variable (s : Set α) variable (A : ℕ → Set α) -- 1ª demostración -- =============== example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by ext x -- x : α -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s calc x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ s ∧ x ∈ ⋃ (i : ℕ), A i := by simp only [mem_inter_iff] _ ↔ x ∈ s ∧ (∃ i : ℕ, x ∈ A i) := by simp only [mem_iUnion] _ ↔ ∃ i : ℕ, x ∈ s ∧ x ∈ A i := by simp only [exists_and_left] _ ↔ ∃ i : ℕ, x ∈ A i ∧ x ∈ s := by simp only [and_comm] _ ↔ ∃ i : ℕ, x ∈ A i ∩ s := by simp only [mem_inter_iff] _ ↔ x ∈ ⋃ (i : ℕ), A i ∩ s := by simp only [mem_iUnion] -- 2ª demostración -- =============== example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by ext x -- x : α -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s constructor . -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i → x ∈ ⋃ (i : ℕ), A i ∩ s intro h -- h : x ∈ s ∩ ⋃ (i : ℕ), A i -- ⊢ x ∈ ⋃ (i : ℕ), A i ∩ s rw [mem_iUnion] -- ⊢ ∃ i, x ∈ A i ∩ s rcases h with ⟨xs, xUAi⟩ -- xs : x ∈ s -- xUAi : x ∈ ⋃ (i : ℕ), A i rw [mem_iUnion] at xUAi -- xUAi : ∃ i, x ∈ A i rcases xUAi with ⟨i, xAi⟩ -- i : ℕ -- xAi : x ∈ A i use i -- ⊢ x ∈ A i ∩ s constructor . -- ⊢ x ∈ A i exact xAi . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ ⋃ (i : ℕ), A i ∩ s → x ∈ s ∩ ⋃ (i : ℕ), A i intro h -- h : x ∈ ⋃ (i : ℕ), A i ∩ s -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i rw [mem_iUnion] at h -- h : ∃ i, x ∈ A i ∩ s rcases h with ⟨i, hi⟩ -- i : ℕ -- hi : x ∈ A i ∩ s rcases hi with ⟨xAi, xs⟩ -- xAi : x ∈ A i -- xs : x ∈ s constructor . -- ⊢ x ∈ s exact xs . -- ⊢ x ∈ ⋃ (i : ℕ), A i rw [mem_iUnion] -- ⊢ ∃ i, x ∈ A i use i -- ⊢ x ∈ A i exact xAi -- 3ª demostración -- =============== example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by ext x -- x : α -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s simp -- ⊢ (x ∈ s ∧ ∃ i, x ∈ A i) ↔ (∃ i, x ∈ A i) ∧ x ∈ s constructor . -- ⊢ (x ∈ s ∧ ∃ i, x ∈ A i) → (∃ i, x ∈ A i) ∧ x ∈ s rintro ⟨xs, ⟨i, xAi⟩⟩ -- xs : x ∈ s -- i : ℕ -- xAi : x ∈ A i -- ⊢ (∃ i, x ∈ A i) ∧ x ∈ s exact ⟨⟨i, xAi⟩, xs⟩ . -- ⊢ (∃ i, x ∈ A i) ∧ x ∈ s → x ∈ s ∧ ∃ i, x ∈ A i rintro ⟨⟨i, xAi⟩, xs⟩ -- xs : x ∈ s -- i : ℕ -- xAi : x ∈ A i -- ⊢ x ∈ s ∧ ∃ i, x ∈ A i exact ⟨xs, ⟨i, xAi⟩⟩ -- 3ª demostración -- =============== example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by ext x -- x : α -- ⊢ x ∈ s ∩ ⋃ (i : ℕ), A i ↔ x ∈ ⋃ (i : ℕ), A i ∩ s aesop -- 4ª demostración -- =============== example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by ext; aesop -- Lemas usados -- ============ -- variable (x : α) -- variable (t : Set α) -- variable (a b : Prop) -- variable (p : α → Prop) -- #check (mem_iUnion : x ∈ ⋃ i, A i ↔ ∃ i, x ∈ A i) -- #check (mem_inter_iff x s t : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t) -- #check (exists_and_left : (∃ (x : α), b ∧ p x) ↔ b ∧ ∃ (x : α), p x) -- #check (and_comm : a ∧ b ↔ b ∧ a) |
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 |
theory Distributiva_de_la_interseccion_respecto_de_la_union_general imports Main begin (* 1ª demostración *) lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))" proof (rule equalityI) show "s ∩ (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. (A i ∩ s))" proof (rule subsetI) fix x assume "x ∈ s ∩ (⋃ i ∈ I. A i)" then have "x ∈ s" by (simp only: IntD1) have "x ∈ (⋃ i ∈ I. A i)" using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by (simp only: IntD2) then show "x ∈ (⋃ i ∈ I. (A i ∩ s))" proof (rule UN_E) fix i assume "i ∈ I" assume "x ∈ A i" then have "x ∈ A i ∩ s" using ‹x ∈ s› by (rule IntI) with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))" by (rule UN_I) qed qed next show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)" proof (rule subsetI) fix x assume "x ∈ (⋃ i ∈ I. A i ∩ s)" then show "x ∈ s ∩ (⋃ i ∈ I. A i)" proof (rule UN_E) fix i assume "i ∈ I" assume "x ∈ A i ∩ s" then have "x ∈ A i" by (rule IntD1) have "x ∈ s" using ‹x ∈ A i ∩ s› by (rule IntD2) moreover have "x ∈ (⋃ i ∈ I. A i)" using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I) ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)" by (rule IntI) qed qed qed (* 2ª demostración *) lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))" proof show "s ∩ (⋃ i ∈ I. A i) ⊆ (⋃ i ∈ I. (A i ∩ s))" proof fix x assume "x ∈ s ∩ (⋃ i ∈ I. A i)" then have "x ∈ s" by simp have "x ∈ (⋃ i ∈ I. A i)" using ‹x ∈ s ∩ (⋃ i ∈ I. A i)› by simp then show "x ∈ (⋃ i ∈ I. (A i ∩ s))" proof fix i assume "i ∈ I" assume "x ∈ A i" then have "x ∈ A i ∩ s" using ‹x ∈ s› by simp with ‹i ∈ I› show "x ∈ (⋃ i ∈ I. (A i ∩ s))" by (rule UN_I) qed qed next show "(⋃ i ∈ I. (A i ∩ s)) ⊆ s ∩ (⋃ i ∈ I. A i)" proof fix x assume "x ∈ (⋃ i ∈ I. A i ∩ s)" then show "x ∈ s ∩ (⋃ i ∈ I. A i)" proof fix i assume "i ∈ I" assume "x ∈ A i ∩ s" then have "x ∈ A i" by simp have "x ∈ s" using ‹x ∈ A i ∩ s› by simp moreover have "x ∈ (⋃ i ∈ I. A i)" using ‹i ∈ I› ‹x ∈ A i› by (rule UN_I) ultimately show "x ∈ s ∩ (⋃ i ∈ I. A i)" by simp qed qed qed (* 3ª demostración *) lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))" by auto end |
