{"id":656,"date":"2021-08-15T06:00:35","date_gmt":"2021-08-15T04:00:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=656"},"modified":"2021-08-06T13:19:33","modified_gmt":"2021-08-06T11:19:33","slug":"la-composicion-de-funciones-suprayectivas-es-suprayectiva","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/la-composicion-de-funciones-suprayectivas-es-suprayectiva\/","title":{"rendered":"La composici\u00f3n de funciones suprayectivas es suprayectiva"},"content":{"rendered":"<p>Demostrar que la composici\u00f3n de dos funciones suprayectivas es una funci\u00f3n suprayectiva.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport tactic\nopen function\n\nvariables {X Y Z : Type}\nvariable  {f : X \u2192 Y}\nvariable  {g : Y \u2192 Z}\n\nexample\n  (hf : surjective f)\n  (hg : surjective g)\n  : surjective (g \u2218 f) :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport tactic\r\nopen function\r\n\r\nvariables {X Y Z : Type}\r\nvariable  {f : X \u2192 Y}\r\nvariable  {g : Y \u2192 Z}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : surjective f)\r\n  (hg : surjective g)\r\n  : surjective (g \u2218 f) :=\r\nbegin\r\n  intro z,\r\n  cases hg z with y hy,\r\n  cases hf y with x hx,\r\n  use x,\r\n  dsimp,\r\n  rw hx,\r\n  exact hy,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : surjective f)\r\n  (hg : surjective g)\r\n  : surjective (g \u2218 f) :=\r\nbegin\r\n  intro z,\r\n  cases hg z with y hy,\r\n  cases hf y with x hx,\r\n  use x,\r\n  calc (g \u2218 f) x = g (f x) : by rw comp_app\r\n             ... = g y     : congr_arg g hx\r\n             ... = z       : hy,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : surjective f)\r\n  (hg : surjective g)\r\n  : surjective (g \u2218 f) :=\r\nassume z,\r\nexists.elim (hg z)\r\n  ( assume y (hy : g y = z),\r\n    exists.elim (hf y)\r\n    ( assume x (hx : f x = y),\r\n      have g (f x) = z, from eq.subst (eq.symm hx) hy,\r\n      show \u2203 x, g (f x) = z, from exists.intro x this))\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : surjective f)\r\n  (hg : surjective g)\r\n  : surjective (g \u2218 f) :=\r\n-- by library_search\r\nsurjective.comp hg hf\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample\r\n  (hf : surjective f)\r\n  (hg : surjective g)\r\n  : surjective (g \u2218 f) :=\r\n\u03bb z, exists.elim (hg z)\r\n  (\u03bb y hy, exists.elim (hf y)\r\n     (\u03bb x hx, exists.intro x\r\n        (show g (f x) = z,\r\n           from (eq.trans (congr_arg g hx) hy))))\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\/La_composicion_de_funciones_suprayectivas_es_suprayectiva.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<p>[expand title=\u00bbSoluciones con Isabelle\/HOL\u00bb]<\/p>\n<pre lang=\"isar\">\r\ntheory La_composicion_de_funciones_suprayectivas_es_suprayectiva\r\nimports Main\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"surj (f :: 'a \u21d2 'b)\"\r\n          \"surj (g :: 'b \u21d2 'c)\"\r\n  shows   \"surj (g \u2218 f)\"\r\nproof (unfold surj_def; intro allI)\r\n  fix z\r\n  obtain y where hy : \"g y = z\"\r\n    using \u2039surj g\u203a by (metis surjD)\r\n  obtain x where hx : \"f x = y\"\r\n    using \u2039surj f\u203a by (metis surjD)\r\n  have \"(g \u2218 f) x = g (f x)\"\r\n    by (simp only: o_apply)\r\n  also have \"\u2026 = g y\"\r\n    by (simp only: \u2039f x = y\u203a)\r\n  also have \"\u2026 = z\"\r\n    by (simp only: \u2039g y = z\u203a)\r\n  finally have \"(g \u2218 f) x = z\"\r\n    by this\r\n  then have \"z = (g \u2218 f) x\"\r\n    by (rule sym)\r\n  then show \"\u2203x. z = (g \u2218 f) x\"\r\n    by (rule exI)\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"surj f\"\r\n          \"surj g\"\r\n  shows   \"surj (g \u2218 f)\"\r\nusing assms image_comp [of g f UNIV]\r\nby (simp only:)\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  assumes \"surj f\"\r\n          \"surj g\"\r\n  shows   \"surj (g \u2218 f)\"\r\nusing assms\r\nby (rule comp_surj)\r\n\r\nend\r\n<\/pre>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Demostrar que la composici\u00f3n de dos funciones suprayectivas es una funci\u00f3n suprayectiva. Para ello, completar la siguiente teor\u00eda de Lean: import tactic open function variables {X Y Z : Type} variable {f : X \u2192 Y} variable {g : Y \u2192 Z} example (hf : surjective f) (hg : surjective g) : surjective (g \u2218 f) := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import tactic open function variables {X Y Z : Type} variable {f : X \u2192 Y} variable {g : Y \u2192 Z} &#8212; 1\u00aa demostraci\u00f3n example (hf : surjective f) (hg : surjective g) : surjective (g \u2218 f) := begin intro z, cases hg z with y hy, cases hf y with x hx, use x, dsimp, rw hx, exact hy, end&#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":[17],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/656"}],"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=656"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/656\/revisions"}],"predecessor-version":[{"id":657,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/656\/revisions\/657"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=656"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=656"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=656"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}