{"id":7463,"date":"2020-10-22T09:37:56","date_gmt":"2020-10-22T07:37:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7463"},"modified":"2020-12-21T09:39:04","modified_gmt":"2020-12-21T08:39:04","slug":"formatus-pruebas-en-lean-de-la-reflexividad-de-la-inclusion-de-conjuntos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-de-la-reflexividad-de-la-inclusion-de-conjuntos\/","title":{"rendered":"ForMatUS: Pruebas en Lean de la reflexividad de la inclusi\u00f3n de conjuntos"},"content":{"rendered":"<p>He a\u00f1adido a la lista <a href=\"https:\/\/bit.ly\/2FcUrwQ\">L\u00f3gica con Lean<\/a> el <a href=\"https:\/\/youtu.be\/uAUAaOKL41A\">v\u00eddeo<\/a> en el que se comentan 11 pruebas en Lean de la propiedad reflexiva de de la inclusi\u00f3n de conjuntos usando los estilos declarativos, aplicativos, funcional y autom\u00e1tico.<\/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\/uAUAaOKL41A\" width=\"560\" height=\"315\" frameborder=\"0\" allowfullscreen=\"allowfullscreen\" data-mce-fragment=\"1\"><\/iframe><\/p>\n<p><\/center>y el <a href=\"https:\/\/github.com\/jaalonso\/Logica_con_Lean\/blob\/master\/src\/3_Conjuntos\/Prueba_de_la_reflexividad_de_la_inclusion_de_conjuntos.lean\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">-- ----------------------------------------------------\n-- Ej. 1. Demostrar\n--    A \u2286 A\n-- ----------------------------------------------------\n\nimport data.set\nvariable  U : Type\nvariable  x : U\nvariables A B C : set U\n\n-- #reduce x \u2208 A\n-- #reduce B \u2286 C\n\n-- 1\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nbegin\n  intros x h,\n  exact h,\nend\n\n-- 2\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nassume x,\nassume h : x \u2208 A,\nshow x \u2208 A, from h\n\n-- 3\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nassume x,\nassume h : x \u2208 A,\nh\n\n-- 4\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nassume x,\n\u03bb h : x \u2208 A, h\n\n-- 5\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nassume x,\nid\n\n-- 6\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\n\u03bb x, id\n\n-- 7\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\n-- by library_search\nset.subset.rfl\n\nopen set\n\n-- 8\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nsubset.rfl\n\n-- 9\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\n-- by hint\nby tauto\n\n-- 10\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nby finish\n\n-- 11\u00aa demostraci\u00f3n\nexample : A \u2286 A :=\nby refl\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>He a\u00f1adido a la lista L\u00f3gica con Lean el v\u00eddeo en el que se comentan 11 pruebas en Lean de la propiedad reflexiva de de la inclusi\u00f3n de conjuntos usando los estilos declarativos, aplicativos, funcional y autom\u00e1tico. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de la teor\u00eda utilizada &#8212; &#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;&#8212;- &#8212; Ej. 1&#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":[166,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\/7463"}],"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=7463"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7463\/revisions"}],"predecessor-version":[{"id":7464,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7463\/revisions\/7464"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7463"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7463"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7463"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}