esta sesi\u00f3n con Lean<\/a>.<\/p>\nEn los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="lean"> y otra con <\/pre>
\n[\/expand]<\/p>\n
[expand title=\"Soluciones con Isabelle\/HOL\"]<\/p>\n
\r\ntheory Propiedad_de_la_densidad_de_los_reales\r\nimports Main HOL.Real\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n fixes x y :: real\r\n assumes \"\u2200 z. y < z \u27f6 x \u2264 z\"\r\n shows \"x \u2264 y\"\r\nproof (rule linorder_class.leI; intro notI)\r\n assume \"y < x\"\r\n then have \"\u2203z. y < z \u2227 z < x\"\r\n by (rule dense)\r\n then obtain a where ha : \"y < a \u2227 a < x\"\r\n by (rule exE)\r\n have \"\u00ac a < a\"\r\n by (rule order.irrefl)\r\n moreover\r\n have \"a < a\"\r\n proof -\r\n have \"y < a \u27f6 x \u2264 a\"\r\n using assms by (rule allE)\r\n moreover\r\n have \"y < a\"\r\n using ha by (rule conjunct1)\r\n ultimately have \"x \u2264 a\"\r\n by (rule mp)\r\n moreover\r\n have \"a < x\"\r\n using ha by (rule conjunct2)\r\n ultimately show \"a < a\"\r\n by (simp only: less_le_trans)\r\n qed\r\n ultimately show False\r\n by (rule notE)\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n fixes x y :: real\r\n assumes \"\u22c0 z. y < z \u27f9 x \u2264 z\"\r\n shows \"x \u2264 y\"\r\nproof (rule linorder_class.leI; intro notI)\r\n assume \"y < x\"\r\n then have \"\u2203z. y < z \u2227 z < x\"\r\n by (rule dense)\r\n then obtain a where hya : \"y < a\" and hax : \"a < x\"\r\n by auto\r\n have \"\u00ac a < a\"\r\n by (rule order.irrefl)\r\n moreover\r\n have \"a < a\"\r\n proof -\r\n have \"a < x\"\r\n using hax .\r\n also have \"\u2026 \u2264 a\"\r\n using assms[OF hya] .\r\n finally show \"a < a\" .\r\n qed\r\n ultimately show False\r\n by (rule notE)\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n fixes x y :: real\r\n assumes \"\u22c0 z. y < z \u27f9 x \u2264 z\"\r\n shows \"x \u2264 y\"\r\nproof (rule linorder_class.leI; intro notI)\r\n assume \"y < x\"\r\n then have \"\u2203z. y < z \u2227 z < x\"\r\n by (rule dense)\r\n then obtain a where hya : \"y < a\" and hax : \"a < x\"\r\n by auto\r\n have \"\u00ac a < a\"\r\n by (rule order.irrefl)\r\n moreover\r\n have \"a < a\"\r\n using hax assms[OF hya] by (rule less_le_trans)\r\n ultimately show False\r\n by (rule notE)\r\nqed\r\n\r\n(* 4\u00aa demostraci\u00f3n *)\r\nlemma\r\n fixes x y :: real\r\n assumes \"\u22c0 z. y < z \u27f9 x \u2264 z\"\r\n shows \"x \u2264 y\"\r\nby (meson assms dense not_less)\r\n\r\n(* 5\u00aa demostraci\u00f3n *)\r\nlemma\r\n fixes x y :: real\r\n assumes \"\u22c0 z. y < z \u27f9 x \u2264 z\"\r\n shows \"x \u2264 y\"\r\nusing assms by (rule dense_ge)\r\n\r\n(* 6\u00aa demostraci\u00f3n *)\r\nlemma\r\n fixes x y :: real\r\n assumes \"\u2200 z. y < z \u27f6 x \u2264 z\"\r\n shows \"x \u2264 y\"\r\nusing assms by (simp only: dense_ge)\r\n\r\nend\r\n<\/pre>\nEn los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>
\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"
Sean x, y n\u00fameros reales tales que \u2200 z, y < z \u2192 x \u2264 z Demostrar que x \u2264 y. Para ello, completar la siguiente teor\u00eda de Lean: import data.real.basic variables {x y : \u211d} example (h : \u2200 z, y < z \u2192 x \u2264 z) : x \u2264 y := sorry [expand title=\"Soluciones con Lean\"] import data.real.basic variables {x y : \u211d} -- 1\u00aa demostraci\u00f3n example (h : \u2200 z, y < z \u2192 x \u2264 z) : x \u2264 y := begin apply le_of_not_gt, intro hxy, cases (exists_between hxy) with a ha, apply (lt_irrefl a), calc a < x : ha.2 ... \u2264 a : h a ha.1, end -- 2\u00aa demostraci\u00f3n example (h : \u2200 z, y < z \u2192...\n<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[24],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/604"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=604"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/604\/revisions"}],"predecessor-version":[{"id":605,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/604\/revisions\/605"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=604"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=604"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=604"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}