{"id":7556,"date":"2021-01-11T10:52:12","date_gmt":"2021-01-11T09:52:12","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7556"},"modified":"2021-01-11T10:54:26","modified_gmt":"2021-01-11T09:54:26","slug":"formatus-pruebas-en-lean-de-hay-infinitos-terminos-de-u-arbitariamente-proximos-a-los-puntos-de-acumulacion","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-de-hay-infinitos-terminos-de-u-arbitariamente-proximos-a-los-puntos-de-acumulacion\/","title":{"rendered":"ForMatUS: Pruebas en Lean de &#8220;Hay infinitos t\u00e9rminos arbitrariamente pr\u00f3ximos a los puntos de acumulaci\u00f3n&#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\/qegIH9fxn8Q\">v\u00eddeo<\/a> en el que se comentan 14 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>\n  Si a es un punto de acumulaci\u00f3n de la sucesi\u00f3n u, entonces<\/p>\n<blockquote><p>\n    \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n &#8211; a| \u2264 \u03b5\n  <\/p><\/blockquote>\n<\/blockquote>\n<p>usando los estilos declarativo, aplicativo 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\/qegIH9fxn8Q\" 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\/2MTc6NC\">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\n-- ----------------------------------------------------\n-- Ejercicio 1. Definir la funci\u00f3n\n--    punto_acumulacion : (\u2115 \u2192 \u211d) \u2192 \u211d \u2192 Prop\n-- tal que (punto_acumulacion u a) expresa que a es un\n-- punto de acumulaci\u00f3n de u; es decir, que es el\n-- l\u00edmite de alguna subsucesi\u00f3n de u.\n-- ----------------------------------------------------\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\n-- ----------------------------------------------------\n-- Ejercicio 2. Demostrar que si a es un punto de\n-- acumulaci\u00f3n de u, entonces\n--    \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\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  -- unfold punto_acumulacion at h,\n  rcases h with \u27e8\u03c6, h\u03c61, h\u03c62\u27e9,\n  -- unfold limite at h\u03c62,\n  cases h\u03c62 \u03b5 h\u03b5 with N' hN',\n  rcases extraccion_mye h\u03c61 N N' with \u27e8m, hm, hm'\u27e9,\n  -- clear h\u03c61 h\u03c62,\n  use \u03c6 m,\n  split,\n  { exact hm', },\n  { exact hN' m hm, },\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample\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  use \u03c6 m,\n  exact \u27e8hm', hN' m hm\u27e9,\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample\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\n-- 4\u00aa demostraci\u00f3n\nexample\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  use \u03c6 m ; finish\nend\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        have h1 : \u2203 n \u2265 N', \u03c6 n \u2265 N,\n          from extraccion_mye h\u03c6.1 N N',\n        exists.elim h1\n          ( assume m,\n            assume hm : \u2203 (H : m \u2265 N'), \u03c6 m \u2265 N,\n            exists.elim hm\n              ( assume hm1 : m \u2265 N',\n                assume hm2 : \u03c6 m \u2265 N,\n                have h2 : |u (\u03c6 m) - a| \u2264 \u03b5,\n                  from hN' m hm1,\n                show \u2203 n \u2265 N, |u n - a| \u2264 \u03b5,\n                  from exists.intro (\u03c6 m) (exists.intro hm2 h2)))))\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        have h1 : \u2203 n \u2265 N', \u03c6 n \u2265 N,\n          from extraccion_mye h\u03c6.1 N N',\n        exists.elim h1\n          ( assume m,\n            assume hm : \u2203 (H : m \u2265 N'), \u03c6 m \u2265 N,\n            exists.elim hm\n              ( assume hm1 : m \u2265 N',\n                assume hm2 : \u03c6 m \u2265 N,\n                have h2 : |u (\u03c6 m) - a| \u2264 \u03b5,\n                  from hN' m hm1,\n                show \u2203 n \u2265 N, |u n - a| \u2264 \u03b5,\n                  from \u27e8\u03c6 m, hm2, h2\u27e9))))\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        have h1 : \u2203 n \u2265 N', \u03c6 n \u2265 N,\n          from extraccion_mye h\u03c6.1 N N',\n        exists.elim h1\n          ( assume m,\n            assume hm : \u2203 (H : m \u2265 N'), \u03c6 m \u2265 N,\n            exists.elim hm\n              ( assume hm1 : m \u2265 N',\n                assume hm2 : \u03c6 m \u2265 N,\n                have h2 : |u (\u03c6 m) - a| \u2264 \u03b5,\n                  from hN' m hm1,\n                \u27e8\u03c6 m, hm2, h2\u27e9))))\n\n-- 8\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        have h1 : \u2203 n \u2265 N', \u03c6 n \u2265 N,\n          from extraccion_mye h\u03c6.1 N N',\n        exists.elim h1\n          ( assume m,\n            assume hm : \u2203 (H : m \u2265 N'), \u03c6 m \u2265 N,\n            exists.elim hm\n              ( assume hm1 : m \u2265 N',\n                assume hm2 : \u03c6 m \u2265 N,\n                \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\n\n-- 9\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        have h1 : \u2203 n \u2265 N', \u03c6 n \u2265 N,\n          from extraccion_mye h\u03c6.1 N N',\n        exists.elim h1\n          ( assume m,\n            assume hm : \u2203 (H : m \u2265 N'), \u03c6 m \u2265 N,\n            exists.elim hm\n              (\u03bb hm1 hm2, \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\n\n-- 10\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        have h1 : \u2203 n \u2265 N', \u03c6 n \u2265 N,\n          from extraccion_mye h\u03c6.1 N N',\n        exists.elim h1\n          (\u03bb m hm, exists.elim hm (\u03bb hm1 hm2, \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\n\n-- 11\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      ( assume N',\n        assume hN' : \u2200 (n : \u2115), n \u2265 N' \u2192 |(u \u2218 \u03c6) n - a| \u2264 \u03b5,\n        exists.elim (extraccion_mye h\u03c6.1 N N')\n          (\u03bb m hm, exists.elim hm (\u03bb hm1 hm2, \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\n\n-- 12\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  ( assume \u03c6,\n    assume h\u03c6 : extraccion \u03c6 \u2227 limite (u \u2218 \u03c6) a,\n    exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n      (\u03bb N' hN', exists.elim (extraccion_mye h\u03c6.1 N N')\n        (\u03bb m hm, exists.elim hm\n          (\u03bb hm1 hm2, \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\n\n-- 13\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\nassume \u03b5,\nassume h\u03b5 : \u03b5 > 0,\nassume N,\nexists.elim h\n  (\u03bb \u03c6 h\u03c6, exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n    (\u03bb N' hN', exists.elim (extraccion_mye h\u03c6.1 N N')\n      (\u03bb m hm, exists.elim hm\n        (\u03bb hm1 hm2, \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\n\n-- 14\u00aa demostraci\u00f3n\nexample\n  (h : punto_acumulacion u a)\n  : \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n - a| \u2264 \u03b5 :=\n\u03bb \u03b5 h\u03b5 N, exists.elim h\n  (\u03bb \u03c6 h\u03c6, exists.elim (h\u03c6.2 \u03b5 h\u03b5)\n    (\u03bb N' hN', exists.elim (extraccion_mye h\u03c6.1 N N')\n      (\u03bb m hm, exists.elim hm\n        (\u03bb hm1 hm2, \u27e8\u03c6 m, hm2, hN' m hm1\u27e9))))\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 14 pruebas en Lean de la propiedad Si a es un punto de acumulaci\u00f3n de la sucesi\u00f3n u, entonces \u2200 \u03b5 > 0, \u2200 N, \u2203 n \u2265 N, |u n &#8211; a| \u2264 \u03b5 usando&#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\/7556"}],"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=7556"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7556\/revisions"}],"predecessor-version":[{"id":7559,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7556\/revisions\/7559"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7556"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7556"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7556"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}