Las relaciones definidas por particiones son simétricas
Este ejercicio es el 11º 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.
Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
Demostrar que la relación definida por una partición es simétrica.
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 |
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} variables {X Y : set A} variable {P : particion A} def relacion : (particion A) → (A → A → Prop) := λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X example (P : particion A) : symmetric (relacion P) := sorry |
[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 69 70 71 72 73 74 75 76 77 78 79 |
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} variables {X Y : set A} variable {P : particion A} def relacion : (particion A) → (A → A → Prop) := λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X -- Se usarán los siguientes lemas auxiliares 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⟩ 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 -- 1ª demostración example (P : particion A) : symmetric (relacion P) := begin rw symmetric, intros a b hab, unfold relacion at *, intros X hX hbX, obtain ⟨Y, hY, haY⟩ := Hrecubren P a, specialize hab Y hY haY, exact pertenece_si_pertenece hY hX hab hbX haY, end -- 2ª demostración example (P : particion A) : symmetric (relacion P) := begin intros a b hab, intros X hX hbX, obtain ⟨Y, hY, haY⟩ := Hrecubren P a, specialize hab Y hY haY, exact pertenece_si_pertenece hY hX hab hbX haY, end -- 3ª demostración lemma simetrica (P : particion A) : symmetric (relacion P) := begin intros a b h X hX hbX, obtain ⟨Y, hY, haY⟩ := Hrecubren P a, specialize h Y hY haY, exact pertenece_si_pertenece hY hX h hbX haY, 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]