(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)
Demostrar con Lean4 que
\[ (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u) \]
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 u : Set α) example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by sorry |
1. Demostración en lenguaje natural
Sea \(x ∈ (s ∩ t) ∪ (s ∩ u)\). Entonces son posibles dos casos.
1º caso: Supongamos que \(x ∈ s ∩ t\). Entonces, \(x ∈ s\) y \(x ∈ t\) (y, por tanto, \(x ∈ t ∪ u\)). Luego, \(x ∈ s ∩ (t ∪ u)\).
2º caso: Supongamos que \(x ∈ s ∩ u\). Entonces, \(x ∈ s\) y \(x ∈ u\) (y, por tanto, \(x ∈ t ∪ u\)). Luego, \(x ∈ s ∩ (t ∪ u)\).
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 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t u : Set α) -- 1ª demostración -- =============== example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by intros x hx -- x : α -- hx : x ∈ s ∩ t ∪ s ∩ u -- ⊢ x ∈ s ∩ (t ∪ u) rcases hx with (xst | xsu) . -- xst : x ∈ s ∩ t constructor . -- ⊢ x ∈ s exact xst.1 . -- ⊢ x ∈ t ∪ u left -- ⊢ x ∈ t exact xst.2 . -- xsu : x ∈ s ∩ u constructor . -- ⊢ x ∈ s exact xsu.1 . -- ⊢ x ∈ t ∪ u right -- ⊢ x ∈ u exact xsu.2 -- 2ª demostración -- =============== example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by rintro x (⟨xs, xt⟩ | ⟨xs, xu⟩) . -- x : α -- xs : x ∈ s -- xt : x ∈ t -- ⊢ x ∈ s ∩ (t ∪ u) use xs -- ⊢ x ∈ t ∪ u left -- ⊢ x ∈ t exact xt . -- x : α -- xs : x ∈ s -- xu : x ∈ u -- ⊢ x ∈ s ∩ (t ∪ u) use xs -- ⊢ x ∈ t ∪ u right -- ⊢ x ∈ u exact xu -- 3ª demostración -- =============== example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by rw [inter_distrib_left s t u] -- 4ª demostración -- =============== example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):= by intros x hx -- x : α -- hx : x ∈ s ∩ t ∪ s ∩ u -- ⊢ x ∈ s ∩ (t ∪ u) aesop |
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 |
theory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2 imports Main begin (* 1ª demostración *) lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" proof (rule subsetI) fix x assume "x ∈ (s ∩ t) ∪ (s ∩ u)" then show "x ∈ s ∩ (t ∪ u)" proof (rule UnE) assume xst : "x ∈ s ∩ t" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ t" using xst by (simp only: IntD2) then have xtu : "x ∈ t ∪ u" by (simp only: UnI1) show "x ∈ s ∩ (t ∪ u)" using xs xtu by (simp only: IntI) next assume xsu : "x ∈ s ∩ u" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ u" using xsu by (simp only: IntD2) then have xtu : "x ∈ t ∪ u" by (simp only: UnI2) show "x ∈ s ∩ (t ∪ u)" using xs xtu by (simp only: IntI) qed qed (* 2ª demostración *) lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" proof fix x assume "x ∈ (s ∩ t) ∪ (s ∩ u)" then show "x ∈ s ∩ (t ∪ u)" proof assume xst : "x ∈ s ∩ t" then have xs : "x ∈ s" by simp have xt : "x ∈ t" using xst by simp then have xtu : "x ∈ t ∪ u" by simp show "x ∈ s ∩ (t ∪ u)" using xs xtu by simp next assume xsu : "x ∈ s ∩ u" then have xs : "x ∈ s" by (simp only: IntD1) have xt : "x ∈ u" using xsu by simp then have xtu : "x ∈ t ∪ u" by simp show "x ∈ s ∩ (t ∪ u)" using xs xtu by simp qed qed (* 3ª demostración *) lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" proof fix x assume "x ∈ (s ∩ t) ∪ (s ∩ u)" then show "x ∈ s ∩ (t ∪ u)" proof assume "x ∈ s ∩ t" then show "x ∈ s ∩ (t ∪ u)" by simp next assume "x ∈ s ∩ u" then show "x ∈ s ∩ (t ∪ u)" by simp qed qed (* 4ª demostración *) lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" proof fix x assume "x ∈ (s ∩ t) ∪ (s ∩ u)" then show "x ∈ s ∩ (t ∪ u)" by auto qed (* 5ª demostración *) lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" by auto (* 6ª demostración *) lemma "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" by (simp only: distrib_inf_le) end |