Pertenencia a bloques de una partición con elementos comunes
Este ejercicio es el 2º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X
es isomorfo al tipo de las relaciones de equivalencia sobre X
.
El anterior es Igualdad de bloques de una partición cuando tienen elementos comunes.
El ejercicio consiste en demostrar que si dos bloques de una partición tienen elementos comunes, entonces los elementos de uno también pertenecen al otro.
Para ello, completar la siguiente teoría de Lean:
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 |
import tactic @[ext] structure particion (A : Type) := (Bloques : set (set A)) (Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty) (Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X) (Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y) namespace particion variable {A : Type} variable {P : particion A} variables {X Y : set A} example (hX : X ∈ Bloques P) (hY : Y ∈ Bloques P) {a b : A} (haX : a ∈ X) (haY : a ∈ Y) (hbX : b ∈ X) : b ∈ Y := sorry end particion |
[expand title=»Soluciones con Lean»]
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 |
import tactic @[ext] structure particion (A : Type) := (Bloques : set (set A)) (Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty) (Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X) (Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y) namespace particion variable {A : Type} variable {P : particion A} variables {X Y : set A} lemma iguales_si_comun (hX : X ∈ Bloques P) (hY : Y ∈ Bloques P) {a : A} (haX : a ∈ X) (haY : a ∈ Y) : X = Y := Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩ -- 1ª demostración example (hX : X ∈ Bloques P) (hY : Y ∈ Bloques P) {a b : A} (haX : a ∈ X) (haY : a ∈ Y) (hbX : b ∈ X) : b ∈ Y := begin convert hbX, apply iguales_si_comun hY hX haY, exact haX, end -- 2ª demostración example (hX : X ∈ Bloques P) (hY : Y ∈ Bloques P) {a b : A} (haX : a ∈ X) (haY : a ∈ Y) (hbX : b ∈ X) : b ∈ Y := begin have hXY : X = Y := iguales_si_comun hX hY haX haY, rw ← hXY, exact hbX, end -- 3ª demostración lemma pertenece_si_pertenece (hX : X ∈ Bloques P) (hY : Y ∈ Bloques P) {a b : A} (haX : a ∈ X) (haY : a ∈ Y) (hbX : b ∈ X) : b ∈ Y := begin convert hbX, exact iguales_si_comun hY hX haY haX, end end particion |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]