{"id":844,"date":"2021-10-10T05:00:44","date_gmt":"2021-10-10T03:00:44","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=844"},"modified":"2021-10-03T17:11:00","modified_gmt":"2021-10-03T15:11:00","slug":"las-relaciones-definidas-por-particiones-son-simetricas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/las-relaciones-definidas-por-particiones-son-simetricas\/","title":{"rendered":"Las relaciones definidas por particiones son sim\u00e9tricas"},"content":{"rendered":"

Este ejercicio es el 11\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>.<\/p>\n

Demostrar que la relaci\u00f3n definida por una partici\u00f3n es sim\u00e9trica.<\/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}\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\nexample\n  (P : particion A)\n  : symmetric (relacion P) :=\nsorry\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\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\n-- Se usar\u00e1n los siguientes lemas auxiliares\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\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (P : particion A)\r\n  : symmetric (relacion P) :=\r\nbegin\r\n  rw symmetric,\r\n  intros a b hab,\r\n  unfold relacion at *,\r\n  intros X hX hbX,\r\n  obtain \u27e8Y, hY, haY\u27e9 := Hrecubren P a,\r\n  specialize hab Y hY haY,\r\n  exact pertenece_si_pertenece hY hX hab hbX haY,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (P : particion A)\r\n  : symmetric (relacion P) :=\r\nbegin\r\n  intros a b hab,\r\n  intros X hX hbX,\r\n  obtain \u27e8Y, hY, haY\u27e9 := Hrecubren P a,\r\n  specialize hab Y hY haY,\r\n  exact pertenece_si_pertenece hY hX hab hbX haY,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\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\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 11\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],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/844"}],"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=844"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/844\/revisions"}],"predecessor-version":[{"id":845,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/844\/revisions\/845"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=844"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=844"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=844"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}