{"id":7581,"date":"2021-01-27T12:00:07","date_gmt":"2021-01-27T11:00:07","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7581"},"modified":"2021-03-02T10:35:28","modified_gmt":"2021-03-02T09:35:28","slug":"pruebas-en-lean-de-la-funcion-identidad-no-esta-acotada-superiormente","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/pruebas-en-lean-de-la-funcion-identidad-no-esta-acotada-superiormente\/","title":{"rendered":"Pruebas en Lean de &#8220;La funci\u00f3n identidad no est\u00e1 acotada superiormente&#8221;"},"content":{"rendered":"<p>He a\u00f1adido a la lista <a href=\"https:\/\/bit.ly\/2QwnT30\">DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean<\/a> el <a href=\"https:\/\/youtu.be\/w6sLbvamoLM\">v\u00eddeo<\/a> en el que se comentan 11 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>\n  La funci\u00f3n identidad no est\u00e1 acotada superiormente\n<\/p><\/blockquote>\n<p>usando los estilos aplicativo, declarativo, y funcional.<\/p>\n<p>A continuaci\u00f3n, se muestra el v\u00eddeo<\/p>\n<p><iframe loading=\"lazy\" width=\"560\" height=\"315\" src=\"https:\/\/www.youtube.com\/embed\/w6sLbvamoLM\" frameborder=\"0\" allow=\"accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n<p>y el <a href=\"https:\/\/bit.ly\/3iPOTaZ\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\n-- ----------------------------------------------------\n-- Ejercicio 1. Definir la funci\u00f3n\n--    acotada_superiormente : (\u211d \u2192 \u211d) \u2192 Prop\n-- tal que (acotada_superiormente f) expresa que la\n-- funci\u00f3n f est\u00e1 acotada superiormente.\n-- ----------------------------------------------------\n\ndef acotada_superiormente : (\u211d \u2192 \u211d) \u2192 Prop\n| f := \u2203 M, \u2200 x, f x \u2264 M\n\n-- ----------------------------------------------------\n-- Ejercicio 2. Demostrar que la funci\u00f3n identidad no\n-- est\u00e1 acotada superiormente.\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nbegin\n  unfold acotada_superiormente,\n  unfold id,\n  by_contradiction h,\n  cases h with M hM,\n  specialize hM (M+1),\n  contrapose hM,\n  simp only [not_le],\n  exact lt_add_one M,\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nbegin\n  unfold acotada_superiormente id,\n  push_neg,\n  intro M,\n  use M + 1,\n  linarith,\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nbegin\n  unfold acotada_superiormente id,\n  push_neg,\n  exact no_top,\nend\n\n-- 4\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nhave h2 : \u2203 M, \u2200 x, id x \u2264 M,\n  from h1,\nshow false, from\n  exists.elim h2\n    ( assume M,\n      assume hM : \u2200 x, id x \u2264 M,\n      have h3 : M + 1 \u2264 M,\n        from hM (M+1),\n      have h4 : \u00ac(M < M + 1),\n        from not_lt.mpr h3,\n      have h5 : M < M + 1,\n        from lt_add_one M,\n      show false,\n        from h4 h5)\n\n-- 5\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nhave h2 : \u2203 M, \u2200 x, id x \u2264 M,\n  from h1,\nshow false, from\n  exists.elim h2\n    ( assume M,\n      assume hM : \u2200 x, id x \u2264 M,\n      have h3 : M + 1 \u2264 M,\n        from hM (M+1),\n      have h4 : \u00ac(M < M + 1),\n        from not_lt.mpr h3,\n      have h5 : M < M + 1,\n        from lt_add_one M,\n      h4 h5)\n\n-- 6\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nhave h2 : \u2203 M, \u2200 x, id x \u2264 M,\n  from h1,\nshow false, from\n  exists.elim h2\n    ( assume M,\n      assume hM : \u2200 x, id x \u2264 M,\n      have h3 : M + 1 \u2264 M,\n        from hM (M+1),\n      (not_lt.mpr h3) (lt_add_one M))\n\n-- 7\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nhave h2 : \u2203 M, \u2200 x, id x \u2264 M,\n  from h1,\nshow false, from\n  exists.elim h2\n    ( assume M,\n      assume hM : \u2200 x, id x \u2264 M,\n      (not_lt.mpr (hM (M+1))) (lt_add_one M))\n\n-- 8\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nhave h2 : \u2203 M, \u2200 x, id x \u2264 M,\n  from h1,\nshow false, from\n  exists.elim h2\n    (\u03bb M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))\n\n-- 9\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nhave h2 : \u2203 M, \u2200 x, id x \u2264 M,\n  from h1,\nexists.elim h2\n  (\u03bb M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))\n\n-- 10\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\nassume h1 : acotada_superiormente id,\nexists.elim h1\n  (\u03bb M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))\n\n-- 11\u00aa demostraci\u00f3n\nexample : \u00acacotada_superiormente id :=\n\u03bb h1, exists.elim h1 (\u03bb M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>He a\u00f1adido a la lista DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean el v\u00eddeo en el que se comentan 11 pruebas en Lean de la propiedad La funci\u00f3n identidad no est\u00e1 acotada superiormente usando los estilos aplicativo, declarativo, y funcional. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de la teor\u00eda utilizada import data.real.basic&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[336],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7581"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7581"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7581\/revisions"}],"predecessor-version":[{"id":7584,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7581\/revisions\/7584"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7581"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7581"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7581"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}