He añadido a la lista Lógica con Lean el vídeo en el que se comentan 7 pruebas en Lean de la propiedad antisimétrica de la inclusión de conjuntos 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 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 |
-- ---------------------------------------------------- -- Ej. 1. Demostrar -- A ⊆ B, B ⊆ A ⊢ A = B -- ---------------------------------------------------- import data.set variable U : Type variables A B : set U open set -- 1ª demostración example (h1 : A ⊆ B) (h2 : B ⊆ A) : A = B := begin ext, split, { intro h, exact h1 h, }, { intro h, exact h2 h, }, end -- 2ª demostración example (h1 : A ⊆ B) (h2 : B ⊆ A) : A = B := ext ( assume x, iff.intro ( assume h : x ∈ A, show x ∈ B, from h1 h) ( assume h : x ∈ B, show x ∈ A, from h2 h)) -- 3ª demostración example (h1 : A ⊆ B) (h2 : B ⊆ A) : A = B := ext (λ x, iff.intro (λ h, h1 h) (λ h, h2 h)) -- 4ª demostración example (h1 : A ⊆ B) (h2 : B ⊆ A) : A = B := eq_of_subset_of_subset ( assume x, assume h : x ∈ A, show x ∈ B, from h1 h) ( assume x, assume h : x ∈ B, show x ∈ A, from h2 h) -- 5ª demostración example (h1 : A ⊆ B) (h2 : B ⊆ A) : A = B := eq_of_subset_of_subset h1 h2 -- 6ª demostración example (h1 : A ⊆ B) (h2 : B ⊆ A) : A = B := -- by library_search subset.antisymm h1 h2 |
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 11 pruebas en Lean de la propiedad reflexiva de de la inclusión de conjuntos 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 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 |
-- ---------------------------------------------------- -- Ej. 1. Demostrar -- A ⊆ A -- ---------------------------------------------------- import data.set variable U : Type variable x : U variables A B C : set U -- #reduce x ∈ A -- #reduce B ⊆ C -- 1ª demostración example : A ⊆ A := begin intros x h, exact h, end -- 2ª demostración example : A ⊆ A := assume x, assume h : x ∈ A, show x ∈ A, from h -- 3ª demostración example : A ⊆ A := assume x, assume h : x ∈ A, h -- 4ª demostración example : A ⊆ A := assume x, λ h : x ∈ A, h -- 5ª demostración example : A ⊆ A := assume x, id -- 6ª demostración example : A ⊆ A := λ x, id -- 7ª demostración example : A ⊆ A := -- by library_search set.subset.rfl open set -- 8ª demostración example : A ⊆ A := subset.rfl -- 9ª demostración example : A ⊆ A := -- by hint by tauto -- 10ª demostración example : A ⊆ A := by finish -- 11ª demostración example : A ⊆ A := by refl |