La función `relacionP` es inversa por la derecha de la función `cociente`
Este ejercicio es el 15º 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.
11. Las relaciones definidas por particiones son simétricas.
12. Las relaciones definidas por particiones son transitivas.
13. Aplicación de particiones en relaciones de equivalencia.
14. La función relacionP es inversa por la izquierda de la función cociente
En los ejercicios 9 y 13 se han definido las funciones
|
1 2 |
cociente : {R : A → A → Prop // equivalence R} → particion A relacionP : particion A → {R : A → A → Prop // equivalence R} |
tales que
+ cociente R es el conjunto cociente de la relación de equivalencia R y
+ relacionP P es la relación de equivalencia definida por la partición P de forma que los elementos relacionados son los que pertenecen a los mismos bloques de P.
Demostrar que relacionP es inversa por la derecha de cociente.
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 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 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 |
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} 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, } def relacion : (particion A) → (A → A → Prop) := λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X lemma reflexiva (P : particion A) : reflexive (relacion P) := λ a X hXC haX, haX 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 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 lemma transitiva (P : particion A) : transitive (relacion P) := λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX) def relacionP : particion A → {R : A → A → Prop // equivalence R} := λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X, ⟨reflexiva P, simetrica P, transitiva P⟩⟩ lemma inversa_dcha : function.right_inverse relacionP (@cociente 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 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 |
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} 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, } def relacion : (particion A) → (A → A → Prop) := λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X lemma reflexiva (P : particion A) : reflexive (relacion P) := λ a X hXC haX, haX 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 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 lemma transitiva (P : particion A) : transitive (relacion P) := λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX) def relacionP : particion A → {R : A → A → Prop // equivalence R} := λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X, ⟨reflexiva P, simetrica P, transitiva P⟩⟩ -- 1ª demostración example : function.right_inverse relacionP (@cociente A) := begin unfold function.right_inverse, unfold function.left_inverse, intro P, ext X, simp [cociente], split, { intro h, cases h with a ha, rw ha, rcases Hrecubren P a with ⟨X, hX, haX⟩, convert hX, ext b, rw pertenece_clase_syss, split, { intro hba, rcases Hrecubren P b with ⟨Y, hY, hbY⟩, specialize hba Y hY hbY, convert hbY, exact iguales_si_comun hX hY haX hba, }, { intros hbX Y hY hbY, apply pertenece_si_pertenece hX hY hbX hbY haX, }}, { intro hX, rcases Hno_vacios P X hX with ⟨a, ha⟩, use a, ext b, split, { intro hbX, rw pertenece_clase_syss, intros Y hY hbY, exact pertenece_si_pertenece hX hY hbX hbY ha, }, { rw pertenece_clase_syss, intro hba, rcases Hrecubren P b with ⟨Y, hY, hbY⟩, specialize hba Y hY hbY, exact pertenece_si_pertenece hY hX hba ha hbY, }} end -- 2ª demostración lemma inversa_dcha : function.right_inverse relacionP (@cociente A) := begin intro P, ext X, show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P, split, { rintro ⟨a, rfl⟩, obtain ⟨X, hX, haX⟩ := Hrecubren P a, convert hX, ext b, rw pertenece_clase_syss, split, { intro hba, obtain ⟨Y, hY, hbY⟩ := Hrecubren P b, specialize hba Y hY hbY, convert hbY, exact iguales_si_comun hX hY haX hba, }, { intros hbX Y hY hbY, apply pertenece_si_pertenece hX hY hbX hbY haX, }}, { intro hX, rcases Hno_vacios P X hX with ⟨a, ha⟩, use a, ext b, split, { intro hbX, rw pertenece_clase_syss, intros Y hY hbY, exact pertenece_si_pertenece hX hY hbX hbY ha, }, { rw pertenece_clase_syss, intro hba, obtain ⟨Y, hY, hbY⟩ := Hrecubren P b, specialize hba Y hY hbY, exact pertenece_si_pertenece hY hX hba ha hbY, }} 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]