{"id":7563,"date":"2021-01-13T08:53:22","date_gmt":"2021-01-13T07:53:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7563"},"modified":"2021-01-13T08:53:22","modified_gmt":"2021-01-13T07:53:22","slug":"formatus-pruebas-en-lean-de-el-punto-de-acumulacion-de-las-convergentes-es-su-limite","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-de-el-punto-de-acumulacion-de-las-convergentes-es-su-limite\/","title":{"rendered":"ForMatUS: Pruebas en Lean de &#8220;El punto de acumulaci\u00f3n de las convergentes es su l\u00edmite&#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\/O-e8eAi7x6I\">v\u00eddeo<\/a> en el que se comentan 4 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>\n  Si a es un punto de acumulaci\u00f3n de una sucesi\u00f3n convergente u, entonces a es el l\u00edmite de u.\n<\/p><\/blockquote>\n<p>usando los estilos declarativo, aplicativos 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\/O-e8eAi7x6I\" 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\/2LFM281\">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 b: \u211d}\nvariables (x y : \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\nlemma cero_de_abs_mn_todos\n  (h : \u2200 \u03b5 > 0, |x| \u2264 \u03b5)\n  : x = 0 :=\nabs_eq_zero.mp\n  (eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)\n\nlemma ig_de_abs_sub_mne_todos\n  (h : \u2200 \u03b5 > 0, |x - y| \u2264 \u03b5)\n  : x = y :=\nsub_eq_zero.mp (cero_de_abs_mn_todos (x - y) h)\n\nlemma unicidad_limite\n  (ha : limite u a)\n  (hb : limite u b)\n  : a = b :=\nbegin\n  apply ig_de_abs_sub_mne_todos,\n  intros \u03b5 h\u03b5,\n  cases ha (\u03b5\/2) (by linarith) with Na hNa,\n  cases hb (\u03b5\/2) (by linarith) with Nb hNb,\n  let N := max Na Nb,\n  specialize hNa N (by finish),\n  specialize hNb N (by finish),\n  calc |a - b|\n       = |(a - u N) + (u N - b)| : by ring\n   ... \u2264 |a - u N| + |u N - b|   : by apply abs_add\n   ... = |u N - a| + |u N - b|   : by rw abs_sub\n   ... \u2264 \u03b5                       : by linarith [hNa, hNb]\nend\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\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 limite_subsucesion\n  (h : limite u a)\n  (h\u03c6 : extraccion \u03c6)\n  : limite (u \u2218 \u03c6) a :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nexists.elim (h \u03b5 h\u03b5)\n ( assume N,\n   assume hN : \u2200 n, n \u2265 N \u2192 |u n - a| \u2264 \u03b5,\n   have h1 : \u2200n, n \u2265 N \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n     { assume n,\n       assume hn : n \u2265 N,\n       have h2 : N \u2264 \u03c6 n, from\n         calc N \u2264 n   : hn\n           ... \u2264 \u03c6 n : id_mne_extraccion h\u03c6 n,\n       show |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n         from hN (\u03c6 n) h2,\n     },\n   show \u2203 N, \u2200n, n \u2265 N \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n     from exists.intro N h1)\n\n-- ----------------------------------------------------\n-- Ejercicio. Demostrar que si a es un punto de\n-- acumulaci\u00f3n de una sucesi\u00f3n de l\u00edmite b, entonces a\n-- y b son iguales.\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (ha : punto_acumulacion u a)\n  (hb : limite u b)\n  : a = b :=\nbegin\n  -- unfold punto_acumulacion at ha,\n  rcases ha with \u27e8\u03c6, h\u03c6\u2081, h\u03c6\u2082\u27e9,\n  have h\u03c6\u2083 : limite (u \u2218 \u03c6) b,\n    from limite_subsucesion hb h\u03c6\u2081,\n  exact unicidad_limite h\u03c6\u2082 h\u03c6\u2083,\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (ha : punto_acumulacion u a)\n  (hb : limite u b)\n  : a = b :=\nbegin\n  rcases ha with \u27e8\u03c6, h\u03c6\u2081, h\u03c6\u2082\u27e9,\n  exact unicidad_limite h\u03c6\u2082 (limite_subsucesion hb h\u03c6\u2081),\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (ha : punto_acumulacion u a)\n  (hb : limite u b)\n  : a = b :=\nexists.elim ha\n  (\u03bb \u03c6 h\u03c6, unicidad_limite h\u03c6.2 (limite_subsucesion hb h\u03c6.1))\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (ha : punto_acumulacion u a)\n  (hb : limite u b)\n  : a = b :=\nexists.elim ha\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    have h\u03c6' : limite (u \u2218 \u03c6) b,\n      from limite_subsucesion hb h\u03c6.1,\n    show a = b,\n      from unicidad_limite h\u03c6.2 h\u03c6')\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 4 pruebas en Lean de la propiedad Si a es un punto de acumulaci\u00f3n de una sucesi\u00f3n convergente u, entonces a es el l\u00edmite de u. usando los estilos declarativo, aplicativos y funcional. A continuaci\u00f3n, se&#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\/7563"}],"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=7563"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7563\/revisions"}],"predecessor-version":[{"id":7564,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7563\/revisions\/7564"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7563"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7563"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7563"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}