{"id":855,"date":"2021-10-14T05:00:38","date_gmt":"2021-10-14T03:00:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=855"},"modified":"2021-10-04T17:17:41","modified_gmt":"2021-10-04T15:17:41","slug":"relacionp_inversaderecha","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/relacionp_inversaderecha\/","title":{"rendered":"La funci\u00f3n `relacionP` es inversa por la derecha de la funci\u00f3n `cociente`"},"content":{"rendered":"

Este ejercicio es el 15\u00ba de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X<\/code> es isomorfo al tipo de las relaciones de equivalencia sobre X<\/code>.<\/p>\n

Los anteriores son
\n1. Igualdad de bloques de una partici\u00f3n cuando tienen elementos comunes<\/a>.
\n2. Pertenencia a bloques de una partici\u00f3n con elementos comunes<\/a>.
\n3. Pertenencia a su propia clase de equivalencia<\/a>.
\n4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos<\/a>.
\n5. Las clases de equivalencia son iguales a las de sus elementos<\/a>.
\n6. Las clases de equivalencia son no vac\u00edas<\/a>.
\n7. Las clases de equivalencia recubren el conjunto<\/a>.
\n8. Las clases de equivalencia son disjuntas<\/a>.
\n9. El cociente aplica relaciones de equivalencia en particiones<\/a>.
\n10. Las relaciones definidas por particiones son reflexivas<\/a>.
\n11. Las relaciones definidas por particiones son sim\u00e9tricas<\/a>.
\n12. Las relaciones definidas por particiones son transitivas<\/a>.
\n13. Aplicaci\u00f3n de particiones en relaciones de equivalencia<\/a>.
\n14. La funci\u00f3n relacionP<\/code> es inversa por la izquierda de la funci\u00f3n cociente<\/code><\/a><\/p>\n

En los ejercicios 9<\/a> y 13<\/a> se han definido las funciones<\/p>\n

\n   cociente : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2192 particion A\n   relacionP : particion A \u2192 {R : A \u2192 A \u2192 Prop \/\/ equivalence R}\n<\/pre>\n
tales que
\n+ cociente R<\/code> es el conjunto cociente de la relaci\u00f3n de equivalencia R<\/code> y
\n+ relacionP P<\/code> es la relaci\u00f3n de equivalencia definida por la partici\u00f3n P<\/code> de forma que los elementos relacionados son los que pertenecen a los mismos bloques de P<\/code>.<\/p>\n
Demostrar que relacionP<\/code> es inversa por la derecha de cociente<\/code>.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport tactic\n\n@[ext] structure particion (A : Type) :=\n(Bloques    : set (set A))\n(Hno_vacios : \u2200 X \u2208 Bloques, (X : set A).nonempty)\n(Hrecubren  : \u2200 a, \u2203 X \u2208 Bloques, a \u2208 X)\n(Hdisjuntos : \u2200 X Y \u2208 Bloques, (X \u2229 Y : set A).nonempty \u2192 X = Y)\n\nnamespace particion\n\nvariable  {A : Type}\nvariables {X Y : set A}\nvariable  {P : particion A}\nvariable  (R : A \u2192 A \u2192 Prop)\n\ndef clase (a : A) :=\n  {b : A | R b a}\n\ndef clases : (A \u2192 A \u2192 Prop) \u2192 set (set A) :=\n  \u03bb R, {B : set A | \u2203 x : A, B = clase R x}\n\nlemma pertenece_clase_syss\n  {a b : A}\n  : b \u2208 clase R a \u2194 R b a :=\nby refl\n\nlemma clases_no_vacias\n  (hR: equivalence R)\n  : \u2200 (X : set A), X \u2208 clases R \u2192 X.nonempty :=\nbegin\n  rintros _ \u27e8a, rfl\u27e9,\n  use a,\n  rw pertenece_clase_syss,\n  apply hR.1,\nend\n\nlemma clases_recubren\n  (hR: equivalence R)\n  : \u2200 a, \u2203 X \u2208 clases R, a \u2208 X :=\nbegin\n  intro a,\n  use clase R a,\n  split,\n  { use a, },\n  { exact hR.1 a, },\nend\n\nlemma subclase_si_pertenece\n  {R : A \u2192 A \u2192 Prop}\n  (hR: equivalence R)\n  {a b : A}\n  : a \u2208 clase R b \u2192 clase R a \u2286 clase R b :=\n\u03bb hab z hza, hR.2.2 hza hab\n\nlemma clases_iguales_si_pertenece\n  {R : A \u2192 A \u2192 Prop}\n  (hR: equivalence R)\n  {a b : A}\n  : a \u2208 clase R b \u2192 clase R a = clase R b :=\n\u03bb hab, set.subset.antisymm\n        (subclase_si_pertenece hR hab)\n        (subclase_si_pertenece hR (hR.2.1 hab))\n\nlemma clases_disjuntas\n  (hR: equivalence R)\n  : \u2200 X Y \u2208 clases R, (X \u2229 Y : set A).nonempty \u2192 X = Y :=\nbegin\n  rintros X Y \u27e8a, rfl\u27e9 \u27e8b, rfl\u27e9 \u27e8c, hca, hcb\u27e9,\n  exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),\nend\n\ndef cociente : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2192 particion A :=\n  \u03bb R, { Bloques    := {B : set A | \u2203 x : A, B = clase R.1 x},\n         Hno_vacios := clases_no_vacias R.1 R.2,\n         Hrecubren  := clases_recubren R.1 R.2,\n         Hdisjuntos := clases_disjuntas R.1 R.2, }\n\ndef relacion : (particion A) \u2192 (A \u2192 A \u2192 Prop) :=\n  \u03bb P a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X\n\nlemma reflexiva\n  (P : particion A)\n  : reflexive (relacion P) :=\n\u03bb a X hXC haX, haX\n\nlemma iguales_si_comun\n  (hX : X \u2208 Bloques P)\n  (hY : Y \u2208 Bloques P)\n  {a : A}\n  (haX : a \u2208 X)\n  (haY : a \u2208 Y)\n  : X = Y :=\nHdisjuntos P X Y hX hY \u27e8a, haX, haY\u27e9\n\nlemma pertenece_si_pertenece\n  (hX : X \u2208 Bloques P)\n  (hY : Y \u2208 Bloques P)\n  {a b : A}\n  (haX : a \u2208 X)\n  (haY : a \u2208 Y)\n  (hbX : b \u2208 X)\n  : b \u2208 Y :=\nbegin\n  convert hbX,\n  exact iguales_si_comun hY hX haY haX,\nend\n\nlemma simetrica\n  (P : particion A)\n  : symmetric (relacion P) :=\nbegin\n  intros a b h X hX hbX,\n  obtain \u27e8Y, hY, haY\u27e9 := Hrecubren P a,\n  specialize h Y hY haY,\n  exact pertenece_si_pertenece hY hX h hbX haY,\nend\n\nlemma transitiva\n  (P : particion A)\n  : transitive (relacion P) :=\n\u03bb a b c hab hbc X hX haX, hbc X hX (hab X hX haX)\n\ndef relacionP : particion A \u2192 {R : A \u2192 A \u2192 Prop \/\/ equivalence R} :=\n  \u03bb P, \u27e8\u03bb a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X,\n        \u27e8reflexiva P, simetrica P, transitiva P\u27e9\u27e9\n\nlemma inversa_dcha :\n  function.right_inverse relacionP (@cociente A) :=\nsorry\n\nend particion\n<\/pre>\n
[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport tactic\r\n\r\n@[ext] structure particion (A : Type) :=\r\n(Bloques    : set (set A))\r\n(Hno_vacios : \u2200 X \u2208 Bloques, (X : set A).nonempty)\r\n(Hrecubren  : \u2200 a, \u2203 X \u2208 Bloques, a \u2208 X)\r\n(Hdisjuntos : \u2200 X Y \u2208 Bloques, (X \u2229 Y : set A).nonempty \u2192 X = Y)\r\n\r\nnamespace particion\r\n\r\nvariable  {A : Type}\r\nvariables {X Y : set A}\r\nvariable  {P : particion A}\r\nvariable  (R : A \u2192 A \u2192 Prop)\r\n\r\ndef clase (a : A) :=\r\n  {b : A | R b a}\r\n\r\ndef clases : (A \u2192 A \u2192 Prop) \u2192 set (set A) :=\r\n  \u03bb R, {B : set A | \u2203 x : A, B = clase R x}\r\n\r\nlemma pertenece_clase_syss\r\n  {a b : A}\r\n  : b \u2208 clase R a \u2194 R b a :=\r\nby refl\r\n\r\nlemma clases_no_vacias\r\n  (hR: equivalence R)\r\n  : \u2200 (X : set A), X \u2208 clases R \u2192 X.nonempty :=\r\nbegin\r\n  rintros _ \u27e8a, rfl\u27e9,\r\n  use a,\r\n  rw pertenece_clase_syss,\r\n  apply hR.1,\r\nend\r\n\r\nlemma clases_recubren\r\n  (hR: equivalence R)\r\n  : \u2200 a, \u2203 X \u2208 clases R, a \u2208 X :=\r\nbegin\r\n  intro a,\r\n  use clase R a,\r\n  split,\r\n  { use a, },\r\n  { exact hR.1 a, },\r\nend\r\n\r\nlemma subclase_si_pertenece\r\n  {R : A \u2192 A \u2192 Prop}\r\n  (hR: equivalence R)\r\n  {a b : A}\r\n  : a \u2208 clase R b \u2192 clase R a \u2286 clase R b :=\r\n\u03bb hab z hza, hR.2.2 hza hab\r\n\r\nlemma clases_iguales_si_pertenece\r\n  {R : A \u2192 A \u2192 Prop}\r\n  (hR: equivalence R)\r\n  {a b : A}\r\n  : a \u2208 clase R b \u2192 clase R a = clase R b :=\r\n\u03bb hab, set.subset.antisymm\r\n        (subclase_si_pertenece hR hab)\r\n        (subclase_si_pertenece hR (hR.2.1 hab))\r\n\r\nlemma clases_disjuntas\r\n  (hR: equivalence R)\r\n  : \u2200 X Y \u2208 clases R, (X \u2229 Y : set A).nonempty \u2192 X = Y :=\r\nbegin\r\n  rintros X Y \u27e8a, rfl\u27e9 \u27e8b, rfl\u27e9 \u27e8c, hca, hcb\u27e9,\r\n  exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),\r\nend\r\n\r\ndef cociente : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2192 particion A :=\r\n  \u03bb R, { Bloques    := {B : set A | \u2203 x : A, B = clase R.1 x},\r\n         Hno_vacios := clases_no_vacias R.1 R.2,\r\n         Hrecubren  := clases_recubren R.1 R.2,\r\n         Hdisjuntos := clases_disjuntas R.1 R.2, }\r\n\r\ndef relacion : (particion A) \u2192 (A \u2192 A \u2192 Prop) :=\r\n  \u03bb P a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X\r\n\r\nlemma reflexiva\r\n  (P : particion A)\r\n  : reflexive (relacion P) :=\r\n\u03bb a X hXC haX, haX\r\n\r\nlemma iguales_si_comun\r\n  (hX : X \u2208 Bloques P)\r\n  (hY : Y \u2208 Bloques P)\r\n  {a : A}\r\n  (haX : a \u2208 X)\r\n  (haY : a \u2208 Y)\r\n  : X = Y :=\r\nHdisjuntos P X Y hX hY \u27e8a, haX, haY\u27e9\r\n\r\nlemma pertenece_si_pertenece\r\n  (hX : X \u2208 Bloques P)\r\n  (hY : Y \u2208 Bloques P)\r\n  {a b : A}\r\n  (haX : a \u2208 X)\r\n  (haY : a \u2208 Y)\r\n  (hbX : b \u2208 X)\r\n  : b \u2208 Y :=\r\nbegin\r\n  convert hbX,\r\n  exact iguales_si_comun hY hX haY haX,\r\nend\r\n\r\nlemma simetrica\r\n  (P : particion A)\r\n  : symmetric (relacion P) :=\r\nbegin\r\n  intros a b h X hX hbX,\r\n  obtain \u27e8Y, hY, haY\u27e9 := Hrecubren P a,\r\n  specialize h Y hY haY,\r\n  exact pertenece_si_pertenece hY hX h hbX haY,\r\nend\r\n\r\nlemma transitiva\r\n  (P : particion A)\r\n  : transitive (relacion P) :=\r\n\u03bb a b c hab hbc X hX haX, hbc X hX (hab X hX haX)\r\n\r\ndef relacionP : particion A \u2192 {R : A \u2192 A \u2192 Prop \/\/ equivalence R} :=\r\n  \u03bb P, \u27e8\u03bb a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X,\r\n        \u27e8reflexiva P, simetrica P, transitiva P\u27e9\u27e9\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  function.right_inverse relacionP (@cociente A) :=\r\nbegin\r\n  unfold function.right_inverse,\r\n  unfold function.left_inverse,\r\n  intro P,\r\n  ext X,\r\n  simp [cociente],\r\n  split,\r\n  { intro h,\r\n    cases h with a ha,\r\n    rw ha,\r\n    rcases Hrecubren P a with \u27e8X, hX, haX\u27e9,\r\n    convert hX,\r\n    ext b,\r\n    rw pertenece_clase_syss,\r\n    split,\r\n    { intro hba,\r\n      rcases Hrecubren P b with \u27e8Y, hY, hbY\u27e9,\r\n      specialize hba Y hY hbY,\r\n      convert hbY,\r\n      exact iguales_si_comun hX hY haX hba, },\r\n    { intros hbX Y hY hbY,\r\n      apply pertenece_si_pertenece hX hY hbX hbY haX, }},\r\n  { intro hX,\r\n    rcases Hno_vacios P X hX with \u27e8a, ha\u27e9,\r\n    use a,\r\n    ext b,\r\n    split,\r\n    { intro hbX,\r\n      rw pertenece_clase_syss,\r\n      intros Y hY hbY,\r\n      exact pertenece_si_pertenece hX hY hbX hbY ha, },\r\n    { rw pertenece_clase_syss,\r\n      intro hba,\r\n      rcases Hrecubren P b with \u27e8Y, hY, hbY\u27e9,\r\n      specialize hba Y hY hbY,\r\n      exact pertenece_si_pertenece hY hX hba ha hbY, }}\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nlemma inversa_dcha :\r\n  function.right_inverse relacionP (@cociente A) :=\r\nbegin\r\n  intro P,\r\n  ext X,\r\n  show (\u2203 (a : A), X = clase _ a) \u2194 X \u2208 Bloques P,\r\n  split,\r\n  { rintro \u27e8a, rfl\u27e9,\r\n    obtain \u27e8X, hX, haX\u27e9 := Hrecubren P a,\r\n    convert hX,\r\n    ext b,\r\n    rw pertenece_clase_syss,\r\n    split,\r\n    { intro hba,\r\n      obtain \u27e8Y, hY, hbY\u27e9 := Hrecubren P b,\r\n      specialize hba Y hY hbY,\r\n      convert hbY,\r\n      exact iguales_si_comun hX hY haX hba, },\r\n    { intros hbX Y hY hbY,\r\n      apply pertenece_si_pertenece hX hY hbX hbY haX, }},\r\n  { intro hX,\r\n    rcases Hno_vacios P X hX with \u27e8a, ha\u27e9,\r\n    use a,\r\n    ext b,\r\n    split,\r\n    { intro hbX,\r\n      rw pertenece_clase_syss,\r\n      intros Y hY hbY,\r\n      exact pertenece_si_pertenece hX hY hbX hbY ha, },\r\n    { rw pertenece_clase_syss,\r\n      intro hba,\r\n      obtain \u27e8Y, hY, hbY\u27e9 := Hrecubren P b,\r\n      specialize hba Y hY hbY,\r\n      exact pertenece_si_pertenece hY hX hba ha hbY, }}\r\nend\r\n\r\nend particion\r\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="lean"> y otra con <\/pre>
\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"
Este ejercicio es el 15\u00ba 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\u00f3n cuando tienen elementos comunes. 2. Pertenencia a bloques de una partici\u00f3n 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\u00edas. 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…<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[281,30],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/855"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=855"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/855\/revisions"}],"predecessor-version":[{"id":858,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/855\/revisions\/858"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=855"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=855"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=855"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}