{"id":7541,"date":"2021-01-05T12:42:35","date_gmt":"2021-01-05T11:42:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7541"},"modified":"2021-01-05T12:42:35","modified_gmt":"2021-01-05T11:42:35","slug":"formatus-pruebas-en-lean-de-la-unicidad-del-limite-de-las-sucesiones","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-de-la-unicidad-del-limite-de-las-sucesiones\/","title":{"rendered":"ForMatUS: Pruebas en Lean de la unicidad del l\u00edmite de las sucesiones"},"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\/nj2xM9s9ygY\">v\u00eddeo<\/a> en el que se comentan pruebas en Lean de la unicidad del l\u00edmite de las sucesiones.<\/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\/nj2xM9s9ygY\" 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\/3b9fyxv\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariables (u : \u2115 \u2192 \u211d)\nvariables (a b x y : \u211d)\n\n-- ----------------------------------------------------\n-- Nota. Se usar\u00e1n las siguientes notaciones,\n-- definiciones y lemas estudiados anteriormente:\n-- + |x| = abs x\n-- + limite u c :\n--      \u2200 \u03b5 > 0, \u2203 N, \u2200 n \u2265 N, |u n - c| \u2264 \u03b5\n-- + cero_de_abs_mn_todos:\n--      (\u2200 \u03b5 > 0, |x| \u2264 \u03b5) \u2192 x = 0\n-- + ig_de_abs_sub_mne_todos:\n--      (\u2200 \u03b5 > 0, |x - y| \u2264 \u03b5) \u2192 x = y\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\n-- ----------------------------------------------------\n-- Ejercicio. Demostrar que cada sucesi\u00f3n tiene como\n-- m\u00e1ximo un l\u00edmite.\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\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) (half_pos h\u03b5) with Na hNa,\n  cases hb (\u03b5\/2) (half_pos h\u03b5) with Nb hNb,\n  let N := max Na Nb,\n  clear ha hb,\n  specialize hNa N (le_max_left  _ _),\n  specialize hNb N (le_max_right  _ _),\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\/2 + \u03b5\/2               : add_le_add hNa hNb\n   ... = \u03b5                       : add_halves \u03b5\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample\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  clear ha hb,\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<\/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 pruebas en Lean de la unicidad del l\u00edmite de las sucesiones. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de la teor\u00eda utilizada import data.real.basic variables (u : \u2115 \u2192 \u211d) variables (a b x&#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\/7541"}],"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=7541"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7541\/revisions"}],"predecessor-version":[{"id":7542,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7541\/revisions\/7542"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7541"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7541"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7541"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}