{"id":7567,"date":"2021-01-16T13:58:51","date_gmt":"2021-01-16T12:58:51","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7567"},"modified":"2021-01-16T13:58:51","modified_gmt":"2021-01-16T12:58:51","slug":"pruebas-en-lean-de-si-u-es-una-sucesion-de-cauchy-y-a-es-un-punto-de-acumulacion-de-u-entonces-a-es-el-limite-de-u","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/pruebas-en-lean-de-si-u-es-una-sucesion-de-cauchy-y-a-es-un-punto-de-acumulacion-de-u-entonces-a-es-el-limite-de-u\/","title":{"rendered":"Pruebas en Lean de &#8220;Si u es una sucesi\u00f3n de Cauchy y a es un punto de acumulaci\u00f3n de u, entonces a es el l\u00edmite de u&#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\/9UEjt4T_4jk\">v\u00eddeo<\/a> en el que se comentan 2 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>\n  Si u es una sucesi\u00f3n de Cauchy y a es un punto de acumulaci\u00f3n de u, entonces a es el l\u00edmite de u.\n<\/p><\/blockquote>\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\/9UEjt4T_4jk\" 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\/3quILr5\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariable  {u : \u2115 \u2192 \u211d}\nvariables {a : \u211d}\nvariable  {\u03c6 : \u2115 \u2192 \u2115}\n\n-- ----------------------------------------------------\n-- Nota. Usaremos los siguientes conceptos estudiados\n-- anteriormente.\n-- ----------------------------------------------------\n\nnotation `|`x`|` := abs x\n\ndef limite : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop :=\n\u03bb u c, \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| \u2264 \u03b5\n\ndef extraccion : (\u2115 \u2192 \u2115) \u2192 Prop\n| \u03c6 := \u2200 n m, n < m \u2192 \u03c6 n < \u03c6 m\n\nlemma id_mne_extraccion\n  (h : extraccion \u03c6)\n  : \u2200 n, n \u2264 \u03c6 n :=\nbegin\n  intros n,\n  induction n with m HI,\n  { linarith },\n  { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },\nend\n\nlemma extraccion_mye\n  (h : extraccion \u03c6)\n  : \u2200 N N', \u2203 n \u2265 N', \u03c6 n \u2265 N :=\n\u03bb N N',\n  \u27e8max N N', le_max_right N N',\n             le_trans (le_max_left N N')\n             (id_mne_extraccion h (max N N'))\u27e9\n\ndef punto_acumulacion : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop\n| u a := \u2203 \u03c6, extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a\n\nlemma cerca_acumulacion\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nbegin\n  intros \u03b5 h\u03b5 N,\n  rcases h with \u27e8\u03c6, h\u03c61, h\u03c62\u27e9,\n  cases h\u03c62 \u03b5 h\u03b5 with N' hN',\n  rcases extraccion_mye h\u03c61 N N' with \u27e8m, hm, hm'\u27e9,\n  exact \u27e8\u03c6 m, hm', hN' _ hm\u27e9,\nend\n\ndef sucesion_de_Cauchy : (\u2115 \u2192 \u211d) \u2192 Prop\n| u := \u2200 \u03b5 > 0, \u2203 N, \u2200 p q, p \u2265 N \u2192 q \u2265 N \u2192 |u p - u q| \u2264 \u03b5\n\n-- ----------------------------------------------------\n-- Ejercicio. Demostrar que si u es una sucesi\u00f3n de\n-- Cauchy y a es un punto de acumulaci\u00f3n de u, entonces\n-- a es el l\u00edmite de u.\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (hu : sucesion_de_Cauchy u)\n  (ha : punto_acumulacion u a)\n  : limite u a :=\nbegin\n  -- unfold limite,\n  intros \u03b5 h\u03b5,\n  -- unfold sucesion_de_Cauchy at hu,\n  cases hu (\u03b5\/2) (half_pos h\u03b5) with N hN,\n  use N,\n  have ha' : \u2203 N' \u2265 N, |u N' - a| \u2264 \u03b5\/2,\n    apply cerca_acumulacion ha (\u03b5\/2) (half_pos h\u03b5),\n  cases ha' with N' h,\n  cases h with hNN' hN',\n  intros n hn,\n  calc   |u n - a|\n       = |(u n - u N') + (u N' - a)| : by ring\n   ... \u2264 |u n - u N'| + |u N' - a|   : abs_add (u n - u N') (u N' - a)\n   ... \u2264 \u03b5\/2 + |u N' - a|            : add_le_add_right (hN n N' hn hNN') _\n   ... \u2264 \u03b5\/2 + \u03b5\/2                   : add_le_add_left hN' (\u03b5 \/ 2)\n   ... = \u03b5                           : add_halves \u03b5\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (hu : sucesion_de_Cauchy u)\n  (ha : punto_acumulacion u a)\n  : limite u a :=\nbegin\n  intros \u03b5 h\u03b5,\n  cases hu (\u03b5\/2) (by linarith) with N hN,\n  use N,\n  have ha' : \u2203 N' \u2265 N, |u N' - a| \u2264 \u03b5\/2,\n    apply cerca_acumulacion ha (\u03b5\/2) (by linarith),\n  rcases ha' with \u27e8N', hNN', hN'\u27e9,\n  intros n hn,\n  calc  |u n - a|\n      = |(u n - u N') + (u N' - a)| : by ring\n  ... \u2264 |u n - u N'| + |u N' - a|   : by simp [abs_add]\n  ... \u2264 \u03b5                           : by linarith [hN n N' hn hNN'],\nend\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 2 pruebas en Lean de la propiedad Si u es una sucesi\u00f3n de Cauchy y a es un punto de acumulaci\u00f3n de u, entonces a es el l\u00edmite de u. A continuaci\u00f3n, se muestra el v\u00eddeo&#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\/7567"}],"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=7567"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7567\/revisions"}],"predecessor-version":[{"id":7568,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7567\/revisions\/7568"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7567"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7567"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7567"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}