{"id":7532,"date":"2021-01-04T06:00:56","date_gmt":"2021-01-04T05:00:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7532"},"modified":"2021-01-03T18:50:46","modified_gmt":"2021-01-03T17:50:46","slug":"formatus-pruebas-en-lean-si-x-%ce%b5-para-todo-%ce%b5-0-entonces-x-0","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-si-x-%ce%b5-para-todo-%ce%b5-0-entonces-x-0\/","title":{"rendered":"ForMatUS: Si |x| < \u03b5, para todo \u03b5 > 0, entonces x = 0"},"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\/YN0F9ldAVCw\">v\u00eddeo<\/a> en el que se comentan 10 pruebas en Lean de la propiedad<\/p>\n<blockquote><p>Si |x| &lt; \u03b5, para todo \u03b5 &gt; 0, entonces x = 0<\/p><\/blockquote>\n<p>usando los estilos declarativos, aplicativos y funcional.<\/p>\n<p>A continuaci\u00f3n, se muestra el v\u00eddeo<\/p>\n<p><center><\/p>\n<p><iframe loading=\"lazy\" src=\"https:\/\/www.youtube.com\/embed\/YN0F9ldAVCw\" width=\"560\" height=\"315\" frameborder=\"0\" allowfullscreen=\"allowfullscreen\" data-mce-fragment=\"1\"><\/iframe><\/p>\n<p><\/center>y el <a href=\"https:\/\/bit.ly\/3b4ErKM\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">\nimport data.real.basic\n\nvariable (x : \u211d)\n\n-- ----------------------------------------------------\n-- Ejercicio 1. Definir la notaci\u00f3n |x| para el valor\n-- absoluto de x.\n-- ----------------------------------------------------\n\nnotation `|`x`|` := abs x\n\n-- ----------------------------------------------------\n-- Ejercicio 2. Demostrar que si |x| < \u03b5, para todo\n-- \u03b5 > 0, entonces x = 0\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nbegin\n  rw \u2190 abs_eq_zero,\n  apply eq_of_le_of_forall_le_of_dense,\n  { exact abs_nonneg x, },\n  { intros \u03b5 h\u03b5,\n    apply le_of_lt,\n    exact h \u03b5 h\u03b5, },\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nbegin\n  rw \u2190 abs_eq_zero,\n  apply eq_of_le_of_forall_le_of_dense,\n  { exact abs_nonneg x, },\n  { intros \u03b5 h\u03b5,\n    exact le_of_lt (h \u03b5 h\u03b5), },\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nbegin\n  rw \u2190 abs_eq_zero,\n  apply eq_of_le_of_forall_le_of_dense,\n  { exact abs_nonneg x, },\n  { exact \u03bb \u03b5 h\u03b5, le_of_lt (h \u03b5 h\u03b5), },\nend\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nbegin\n  rw \u2190 abs_eq_zero,\n  apply eq_of_le_of_forall_le_of_dense\n        (abs_nonneg x)\n        (\u03bb \u03b5 h\u03b5, le_of_lt (h \u03b5 h\u03b5)),\nend\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nabs_eq_zero.mp\n  (eq_of_le_of_forall_le_of_dense\n    (abs_nonneg x)\n    (\u03bb \u03b5 h\u03b5, le_of_lt (h \u03b5 h\u03b5)))\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nhave h1 : 0 \u2264 |x|,\n  from abs_nonneg x,\nhave h2 : \u2200 \u03b5, \u03b5 > 0 \u2192 |x| \u2264 \u03b5,\n  { assume \u03b5,\n    assume h\u03b5 : \u03b5 > 0,\n    have h2a : |x| < \u03b5,\n      from h \u03b5 h\u03b5,\n    show |x| \u2264 \u03b5,\n      from le_of_lt h2a },\nhave h3 : |x| = 0,\n  from eq_of_le_of_forall_le_of_dense h1 h2,\nshow x = 0,\n  from abs_eq_zero.mp h3\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nhave h1 : 0 \u2264 |x|,\n  from abs_nonneg x,\nhave h2 : \u2200 \u03b5, \u03b5 > 0 \u2192 |x| \u2264 \u03b5,\n  { assume \u03b5,\n    assume h\u03b5 : \u03b5 > 0,\n    have h2a : |x| < \u03b5,\n      from h \u03b5 h\u03b5,\n    show |x| \u2264 \u03b5,\n      from le_of_lt h2a },\nhave h3 : |x| = 0,\n  from eq_of_le_of_forall_le_of_dense h1 h2,\nabs_eq_zero.mp h3\n\n-- 8\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nhave h1 : 0 \u2264 |x|,\n  from abs_nonneg x,\nhave h2 : \u2200 \u03b5, \u03b5 > 0 \u2192 |x| \u2264 \u03b5,\n  { assume \u03b5,\n    assume h\u03b5 : \u03b5 > 0,\n    have h2a : |x| < \u03b5,\n      from h \u03b5 h\u03b5,\n    show |x| \u2264 \u03b5,\n      from le_of_lt h2a },\nabs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2)\n\n-- 9\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nhave h1 : 0 \u2264 |x|,\n  from abs_nonneg x,\nhave h2 : \u2200 \u03b5, \u03b5 > 0 \u2192 |x| \u2264 \u03b5,\n  { assume \u03b5,\n    assume h\u03b5 : \u03b5 > 0,\n    show |x| \u2264 \u03b5,\n      from le_of_lt (h \u03b5 h\u03b5) },\nabs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2)\n\n-- 10\u00aa demostraci\u00f3n\nexample\n  (h : \u2200 \u03b5 > 0, |x| < \u03b5)\n  : x = 0 :=\nabs_eq_zero.mp\n  (eq_of_le_of_forall_le_of_dense\n    (abs_nonneg x)\n    (\u03bb \u03b5 h\u03b5, le_of_lt (h \u03b5 h\u03b5)))\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 10 pruebas en Lean de la propiedad Si |x| &lt; \u03b5, para todo \u03b5 &gt; 0, entonces x = 0 usando los estilos declarativos, aplicativos y funcional. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo&#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\/7532"}],"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=7532"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7532\/revisions"}],"predecessor-version":[{"id":7537,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7532\/revisions\/7537"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7532"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7532"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7532"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}