ForMatUS: Pruebas en Lean de (A ∩ Bᶜ) ∪ B = A ∪ B
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad
|
1 |
(A ∩ Bᶜ) ∪ B = A ∪ B |
usando los estilos declarativos, aplicativos, funcional y automático.
A continuación, se muestra el vídeo
|
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 |
-- ---------------------------------------------------- -- Ej. 1. Demostrar -- (A ∩ Bᶜ) ∪ B = A ∪ B -- ---------------------------------------------------- import data.set open set variable U : Type variables A B C : set U -- 1ª demostración -- =============== example : (A ∩ Bᶜ) ∪ B = A ∪ B := calc (A ∩ Bᶜ) ∪ B = (A ∪ B) ∩ (Bᶜ ∪ B) : by rw union_distrib_right ... = (A ∪ B) ∩ univ : by rw compl_union_self ... = A ∪ B : by rw inter_univ example : (A ∩ B) ∪ C = (A ∪ C) ∩ (B ∪ C) := -- by library_search union_distrib_right A B C example : Bᶜ ∪ B = univ := -- by library_search compl_union_self B example : A ∩ univ = A := -- by library_search inter_univ A -- 2ª demostración -- =============== example : (A ∩ Bᶜ) ∪ B = A ∪ B := begin rw union_distrib_right, rw compl_union_self, rw inter_univ, end -- 3ª demostración -- =============== example : (A ∩ Bᶜ) ∪ B = A ∪ B := by rw [union_distrib_right, compl_union_self, inter_univ] -- 4ª demostración -- =============== example : (A ∩ Bᶜ) ∪ B = A ∪ B := by simp [union_distrib_right] |