{"id":7303,"date":"2020-08-30T10:40:59","date_gmt":"2020-08-30T08:40:59","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7303"},"modified":"2020-08-30T10:40:59","modified_gmt":"2020-08-30T08:40:59","slug":"formatus-conectivas-y-desigualdades-en-lean","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-conectivas-y-desigualdades-en-lean\/","title":{"rendered":"ForMatUS: Conectivas y desigualdades en Lean"},"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 v\u00eddeo <a href=\"https:\/\/youtu.be\/vPkse8LMpH0\">Conectivas y desigualdades en Lean<\/a> en el se comentan las demostraciones en Lean de algunas de las propiedades de las desigualdades de los n\u00fameros reales estudiadas en v\u00eddeos anteriores, pero formuladas con conectivas. Concretamente, se demuestran las 5 propiedades siguientes:<\/p>\n<blockquote><p>\n  Sean a, b y c n\u00fameros reales.<\/p>\n<ol>\n<li>0 \u2264 a \u2192 b \u2264 a + b<\/li>\n<li>0 \u2264 b \u2192 a \u2264 a + b<\/li>\n<li>(0 \u2264 a \u2227 0 \u2264 b) \u2192 0 \u2264 a + b<\/li>\n<li>0 \u2264 a \u2192 (0 \u2264 b \u2192 0 \u2264 a + b)<\/li>\n<li>Si (0 \u2264 a \u2227 0 \u2264 b) \u2192 0 \u2264 a + b, entonces  0 \u2264 a \u2192 (0 \u2264 b \u2192 0 \u2264 a + b)<\/li>\n<\/ol>\n<\/blockquote>\n<p>Los enlaces correspondientes son: a la <a href=\"https:\/\/bit.ly\/3b9uIkj\">sesi\u00f3n en Lean Web<\/a>, al <a href=\"https:\/\/bit.ly\/2GasXIq\">c\u00f3digo<\/a> y al <a href=\"https:\/\/bit.ly\/32AyBuQ\">libro &#8220;DAO con Lean&#8221;<\/a>.<\/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\/vPkse8LMpH0\" frameborder=\"0\" allow=\"accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture\" allowfullscreen><\/iframe><\/p>\n","protected":false},"excerpt":{"rendered":"<p>He a\u00f1adido a la lista DAO (Demostraci\u00f3n Asistida por Ordenador) con Lean el v\u00eddeo Conectivas y desigualdades en Lean en el se comentan las demostraciones en Lean de algunas de las propiedades de las desigualdades de los n\u00fameros reales estudiadas en v\u00eddeos anteriores, pero formuladas con conectivas. Concretamente, se demuestran las 5 propiedades siguientes: Sean&#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":[],"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\/7303"}],"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=7303"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7303\/revisions"}],"predecessor-version":[{"id":7304,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7303\/revisions\/7304"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7303"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7303"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7303"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}