ForMatUS: Unión e intersección de familias de conjuntos en Lean
He añadido a la lista Lógica con Lean el vídeo en el que se comentan cómo definir en Lean la unión e intersección de familias de conjuntos y caracterizar la relación de pertenencia.
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 78 79 80 81 82 83 84 85 86 87 88 |
-- ---------------------------------------------------- -- Ej. 1. Declarar I y U como variables de tipo. -- ---------------------------------------------------- variables {I U : Type} -- ---------------------------------------------------- -- Ej. 2. Definir la función -- Union : (I → set U) → set U -- tal que (Union A) es la unión de de los conjuntos de -- la familia A. -- ---------------------------------------------------- def Union (A : I → set U) : set U := { x | ∃ i : I, x ∈ A i } -- ---------------------------------------------------- -- Ej. 3. Definir la función -- Inter : (I → set U) → set U -- tal que (Inter A) es la intersección de de los -- conjuntos de la familia A. -- ---------------------------------------------------- def Inter (A : I → set U) : set U := { x | ∀ i : I, x ∈ A i } -- ---------------------------------------------------- -- Ej. 4. Declarar -- + x como una variable sobre U y -- + A como una variable sobre familas de conjuntos de -- U con índice en A. -- ---------------------------------------------------- variable x : U variable (A : I → set U) -- ---------------------------------------------------- -- Ej. 5. Demostrar que -- x ∈ Union A ⊢ ∃ i, x ∈ A i -- ---------------------------------------------------- example (h : x ∈ Union A) : ∃ i, x ∈ A i := h -- ---------------------------------------------------- -- Ej. 6. Demostrar que -- x ∈ x ∈ Inter A ⊢ ∀ i, x ∈ A i -- ---------------------------------------------------- example (h : x ∈ Inter A) : ∀ i, x ∈ A i := h -- ---------------------------------------------------- -- Ej 7. Usar (⋃ i, A i) como notación para (Union A). -- ---------------------------------------------------- notation `⋃` binders `, ` r:(scoped f, Union f) := r -- ---------------------------------------------------- -- Ej 8. Usar (⋂ i, A i) como notación para (Inter A). -- ---------------------------------------------------- notation `⋂` binders `, ` r:(scoped f, Inter f) := r -- ---------------------------------------------------- -- Ej. 9. Demostrar que -- x ∈ ⋃ i, A i ⊢ ∃ i, x ∈ A i -- ---------------------------------------------------- example (h : x ∈ ⋃ i, A i) : ∃ i, x ∈ A i := h -- ---------------------------------------------------- -- Ej. 10. Demostrar que -- x ∈ x ∈ ⋂ i, A i ⊢ ∀ i, x ∈ A i -- ---------------------------------------------------- example (h : x ∈ ⋂ i, A i) : ∀ i, x ∈ A i := h |