El cociente aplica relaciones de equivalencia en particiones
Este ejercicio es el 9º 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.
El ejercicio consiste en definir la función
|
1 |
cociente : {R : A → A → Prop // equivalence R} → particion A |
tal que cociente R es la partición de A formada por las clases de equivalencia de la relación de equivalencia R.
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} variable (R : A → A → Prop) def clase (a : A) := {b : A | R b a} def clases : (A → A → Prop) → set (set A) := λ R, {B : set A | ∃ x : A, B = clase R x} def cociente : {R : A → A → Prop // equivalence R} → particion A := 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 69 70 71 72 73 74 75 76 77 78 |
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} variable (R : A → A → Prop) def clase (a : A) := {b : A | R b a} def clases : (A → A → Prop) → set (set A) := λ R, {B : set A | ∃ x : A, B = clase R x} lemma pertenece_clase_syss {a b : A} : b ∈ clase R a ↔ R b a := by refl lemma clases_no_vacias (hR: equivalence R) : ∀ (X : set A), X ∈ clases R → X.nonempty := begin rintros _ ⟨a, rfl⟩, use a, rw pertenece_clase_syss, apply hR.1, end lemma clases_recubren (hR: equivalence R) : ∀ a, ∃ X ∈ clases R, a ∈ X := begin intro a, use clase R a, split, { use a, }, { exact hR.1 a, }, end lemma subclase_si_pertenece {R : A → A → Prop} (hR: equivalence R) {a b : A} : a ∈ clase R b → clase R a ⊆ clase R b := λ hab z hza, hR.2.2 hza hab lemma clases_iguales_si_pertenece {R : A → A → Prop} (hR: equivalence R) {a b : A} : a ∈ clase R b → clase R a = clase R b := λ hab, set.subset.antisymm (subclase_si_pertenece hR hab) (subclase_si_pertenece hR (hR.2.1 hab)) lemma clases_disjuntas (hR: equivalence R) : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y := begin rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩, exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb), end def cociente : {R : A → A → Prop // equivalence R} → particion A := λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x}, Hno_vacios := clases_no_vacias R.1 R.2, Hrecubren := clases_recubren R.1 R.2, Hdisjuntos := clases_disjuntas R.1 R.2, } 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]
