{"id":376,"date":"2021-06-04T11:16:43","date_gmt":"2021-06-04T09:16:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=376"},"modified":"2021-06-04T11:28:50","modified_gmt":"2021-06-04T09:28:50","slug":"union-con-interseccion-general","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/union-con-interseccion-general\/","title":{"rendered":"Uni\u00f3n con intersecci\u00f3n general"},"content":{"rendered":"

Demostrar que<\/p>\n

   s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s)\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
import data.set.basic\nimport tactic\n\nopen set\n\nvariable  {\u03b1 : Type}\nvariable  s : set \u03b1\nvariables A : \u2115 \u2192 set \u03b1\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nsorry\n<\/pre>\n
Soluciones<\/h4>\n
<\/p>\n
Soluciones con Lean<\/strong><\/p>\n
import data.set.basic\nimport tactic\n\nopen set\n\nvariable  {\u03b1 : Type}\nvariable  s : set \u03b1\nvariables A : \u2115 \u2192 set \u03b1\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nbegin\n  ext x,\n  simp only [mem_union, mem_Inter],\n  split,\n  { intros h i,\n    cases h with xs xAi,\n    { right,\n      exact xs },\n    { left,\n      exact xAi i, }},\n  { intro h,\n    by_cases xs : x \u2208 s,\n    { left,\n      exact xs },\n    { right,\n      intro i,\n      cases h i with xAi xs,\n      { exact xAi, },\n      { contradiction, }}},\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nbegin\n  ext x,\n  simp only [mem_union, mem_Inter],\n  split,\n  { rintros (xs | xI) i,\n    { right,\n      exact xs },\n    { left,\n      exact xI i }},\n  { intro h,\n    by_cases xs : x \u2208 s,\n    { left,\n      exact xs },\n    { right,\n      intro i,\n      cases h i,\n      { assumption },\n      { contradiction }}},\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nbegin\n  ext x,\n  simp only [mem_union, mem_Inter],\n  split,\n  { finish, },\n  { finish, },\nend\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nbegin\n  ext,\n  simp only [mem_union, mem_Inter],\n  split ; finish,\nend\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nbegin\n  ext,\n  simp only [mem_union, mem_Inter],\n  finish [iff_def],\nend\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) :=\nby finish [ext_iff, mem_union, mem_Inter, iff_def]\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Soluciones con Isabelle\/HOL<\/strong><\/p>\n
theory Union_con_interseccion_general\nimports Main\nbegin\n\nsection \u20391\u00aa demostraci\u00f3n\u203a\n\nlemma \"s \u222a (\u22c2 i \u2208 I. A i) = (\u22c2 i \u2208 I. A i \u222a s)\"\nproof (rule equalityI)\n  show \"s \u222a (\u22c2 i \u2208 I. A i) \u2286 (\u22c2 i \u2208 I. A i \u222a s)\" \n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    then show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n    proof (rule UnE)\n      assume \"x \u2208 s\"\n      show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n      proof (rule INT_I)\n        fix i\n        assume \"i \u2208 I\"\n        show \"x \u2208 A i \u222a s\" \n          using \u2039x \u2208 s\u203a by (rule UnI2)\n      qed \n    next\n      assume h1 : \"x \u2208 (\u22c2 i \u2208 I. A i)\"\n      show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n      proof (rule INT_I)\n        fix i\n        assume \"i \u2208 I\"\n        with h1 have \"x \u2208 A i\" \n          by (rule INT_D)\n        then show \"x \u2208 A i \u222a s\" \n          by (rule UnI1)\n      qed \n    qed\n  qed\nnext\n  show \"(\u22c2 i \u2208 I. A i \u222a s) \u2286 s \u222a (\u22c2 i \u2208 I. A i)\" \n  proof (rule subsetI)\n    fix x\n    assume h2 : \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n    show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    proof (cases \"x \u2208 s\")\n      assume \"x \u2208 s\"\n      then show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\" \n        by (rule UnI1)\n    next\n      assume \"x \u2209 s\"\n      have \"x \u2208 (\u22c2 i \u2208 I. A i)\" \n      proof (rule INT_I)\n        fix i\n        assume \"i \u2208 I\"\n        with h2 have \"x \u2208 A i \u222a s\" \n          by (rule INT_D)\n        then show \"x \u2208 A i\"\n        proof (rule UnE)\n          assume \"x \u2208 A i\"\n          then show \"x \u2208 A i\"\n            by this\n        next\n          assume \"x \u2208 s\"\n          with \u2039x \u2209 s\u203a show \"x \u2208 A i\" \n            by (rule notE)\n        qed\n      qed \n      then show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\" \n        by (rule UnI2)\n    qed\n  qed\nqed\n\nsection \u20392\u00aa demostraci\u00f3n\u203a\n\nlemma \"s \u222a (\u22c2 i \u2208 I. A i) = (\u22c2 i \u2208 I. A i \u222a s)\"\nproof \n  show \"s \u222a (\u22c2 i \u2208 I. A i) \u2286 (\u22c2 i \u2208 I. A i \u222a s)\" \n  proof \n    fix x\n    assume \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    then show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n    proof \n      assume \"x \u2208 s\"\n      show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n      proof \n        fix i\n        assume \"i \u2208 I\"\n        show \"x \u2208 A i \u222a s\" \n          using \u2039x \u2208 s\u203a by simp\n      qed \n    next\n      assume h1 : \"x \u2208 (\u22c2 i \u2208 I. A i)\"\n      show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n      proof \n        fix i\n        assume \"i \u2208 I\"\n        with h1 have \"x \u2208 A i\" \n          by simp\n        then show \"x \u2208 A i \u222a s\" \n          by simp\n      qed \n    qed\n  qed\nnext\n  show \"(\u22c2 i \u2208 I. A i \u222a s) \u2286 s \u222a (\u22c2 i \u2208 I. A i)\" \n  proof \n    fix x\n    assume h2 : \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n    show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    proof (cases \"x \u2208 s\")\n      assume \"x \u2208 s\"\n      then show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\" \n        by simp\n    next\n      assume \"x \u2209 s\"\n      have \"x \u2208 (\u22c2 i \u2208 I. A i)\" \n      proof \n        fix i\n        assume \"i \u2208 I\"\n        with h2 have \"x \u2208 A i \u222a s\" \n          by (rule INT_D)\n        then show \"x \u2208 A i\"\n        proof \n          assume \"x \u2208 A i\"\n          then show \"x \u2208 A i\"\n            by this\n        next\n          assume \"x \u2208 s\"\n          with \u2039x \u2209 s\u203a show \"x \u2208 A i\" \n            by simp\n        qed\n      qed \n      then show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\" \n        by simp\n    qed\n  qed\nqed\n\nsection \u20393\u00aa demostraci\u00f3n\u203a\n\nlemma \"s \u222a (\u22c2 i \u2208 I. A i) = (\u22c2 i \u2208 I. A i \u222a s)\"\nproof \n  show \"s \u222a (\u22c2 i \u2208 I. A i) \u2286 (\u22c2 i \u2208 I. A i \u222a s)\" \n  proof \n    fix x\n    assume \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    then show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n    proof \n      assume \"x \u2208 s\"\n      then show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n        by simp\n    next\n      assume \"x \u2208 (\u22c2 i \u2208 I. A i)\"\n      then show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n        by simp\n    qed\n  qed\nnext\n  show \"(\u22c2 i \u2208 I. A i \u222a s) \u2286 s \u222a (\u22c2 i \u2208 I. A i)\" \n  proof \n    fix x\n    assume h2 : \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n    show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    proof (cases \"x \u2208 s\")\n      assume \"x \u2208 s\"\n      then show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\" \n        by simp\n    next\n      assume \"x \u2209 s\"\n      then show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\" \n        using h2 by simp\n    qed\n  qed\nqed\n\nsection \u20394\u00aa demostraci\u00f3n\u203a\n\nlemma \"s \u222a (\u22c2 i \u2208 I. A i) = (\u22c2 i \u2208 I. A i \u222a s)\"\nproof \n  show \"s \u222a (\u22c2 i \u2208 I. A i) \u2286 (\u22c2 i \u2208 I. A i \u222a s)\" \n  proof \n    fix x\n    assume \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    then show \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\" \n    proof \n      assume \"x \u2208 s\"\n      then show ?thesis by simp\n    next\n      assume \"x \u2208 (\u22c2 i \u2208 I. A i)\"\n      then show ?thesis by simp\n    qed\n  qed\nnext\n  show \"(\u22c2 i \u2208 I. A i \u222a s) \u2286 s \u222a (\u22c2 i \u2208 I. A i)\" \n  proof \n    fix x\n    assume h2 : \"x \u2208 (\u22c2 i \u2208 I. A i \u222a s)\"\n    show \"x \u2208 s \u222a (\u22c2 i \u2208 I. A i)\"\n    proof (cases \"x \u2208 s\")\n      case True\n      then show ?thesis by simp\n    next\n      case False\n      then show ?thesis using h2 by simp\n    qed\n  qed\nqed\n\nsection \u20395\u00aa demostraci\u00f3n\u203a\n\nlemma \"s \u222a (\u22c2 i \u2208 I. A i) = (\u22c2 i \u2208 I. A i \u222a s)\"\n  by auto\n\n\nend\n<\/pre>\n
Nuevas soluciones<\/strong><\/p>\n
    \n
  • En los comentarios se pueden escribir nuevas soluciones.<\/li>\n
  • El c\u00f3digo se debe escribir entre una l\u00ednea con <pre lang=\u00bbisar\u00bb> y otra con <\/pre><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"
    Demostrar que s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) Para ello, completar la siguiente teor\u00eda de Lean: import data.set.basic import tactic open set variable {\u03b1 : Type} variable s : set \u03b1 variables A : \u2115 \u2192 set \u03b1 example : s \u222a (\u22c2 i, A i) = \u22c2 i, (A i \u222a s) := sorry Soluciones<\/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":[7],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/376"}],"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=376"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/376\/revisions"}],"predecessor-version":[{"id":382,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/376\/revisions\/382"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=376"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=376"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=376"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}