{"id":798,"date":"2021-10-01T05:00:13","date_gmt":"2021-10-01T03:00:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=798"},"modified":"2021-10-02T12:30:02","modified_gmt":"2021-10-02T10:30:02","slug":"pertenencia-a-bloques-de-una-particion-con-elementos-comunes","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/pertenencia-a-bloques-de-una-particion-con-elementos-comunes\/","title":{"rendered":"Pertenencia a bloques de una partici\u00f3n con elementos comunes"},"content":{"rendered":"<p>Este ejercicio es el 2\u00ba de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto <code>X<\/code> es isomorfo al tipo de las relaciones de equivalencia sobre <code>X<\/code>.<\/p>\n<p>El anterior es <a href=\"https:\/\/bit.ly\/2YfsvBZ\">Igualdad de bloques de una partici\u00f3n cuando tienen elementos comunes<\/a>.<\/p>\n<p>El ejercicio consiste en demostrar que si dos bloques de una partici\u00f3n tienen elementos comunes, entonces los elementos de uno tambi\u00e9n pertenecen al otro.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\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}\nvariable  {P : particion A}\nvariables {X Y : set A}\n\nexample\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 :=\nsorry\n\nend particion\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\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\nvariable  {P : particion A}\r\nvariables {X Y : set A}\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\n-- 1\u00aa demostraci\u00f3n\r\nexample\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  apply iguales_si_comun hY hX haY,\r\n  exact haX,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\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  have hXY : X = Y := iguales_si_comun hX hY haX haY,\r\n  rw \u2190 hXY,\r\n  exact hbX,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\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\nend particion\r\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Pertenencia_a_bloques_de_una_particion_con_elementos_comunes.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Este ejercicio es el 2\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. El anterior es Igualdad de bloques de una partici\u00f3n cuando tienen elementos comunes. El ejercicio consiste en demostrar que si dos bloques de una partici\u00f3n tienen elementos comunes, entonces los elementos de uno tambi\u00e9n pertenecen al otro. Para ello, completar la siguiente teor\u00eda de Lean: import tactic @[ext] structure particion (A : Type) := (Bloques : set (set A)) (Hno_vacios : \u2200 X \u2208 Bloques, (X : set A).nonempty) (Hrecubren : \u2200 a, \u2203 X \u2208 Bloques, a \u2208 X) (Hdisjuntos : \u2200 X Y \u2208 Bloques, (X \u2229 Y : set&#8230;<\/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\/798"}],"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=798"}],"version-history":[{"count":8,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/798\/revisions"}],"predecessor-version":[{"id":828,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/798\/revisions\/828"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=798"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=798"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=798"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}