{"id":1478,"date":"2023-08-23T06:00:56","date_gmt":"2023-08-23T04:00:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1478"},"modified":"2023-08-07T11:45:14","modified_gmt":"2023-08-07T09:45:14","slug":"23-ago-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/23-ago-23\/","title":{"rendered":"En \u211d, si a \u2264 b, b < c, c \u2264 d y d < e, entonces a < e"},"content":{"rendered":"


\nDemostrar con Lean4 que si \\(a\\), \\(b\\), \\(c\\), \\(d\\) y \\(e\\) son n\u00fameros reales tales \\(a \\leq b\\), \\(b < c\\), \\(c \\leq d\\) y \\(d < e\\), entonces \\(a < e\\).\n\nPara ello, completar la siguiente teor\u00eda de Lean4:\n\n\n\n

\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b c d e : \u211d)\r\n\r\nexample\r\n  (h1 : a \u2264 b)\r\n  (h2 : b < c)\r\n  (h3 : c \u2264 d)\r\n  (h4 : d < e) :\r\n  a < e :=\r\nsorry\r\n<\/pre>\n
<\/p>\n
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n
1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de desigualdades
\n\\begin{align}
\n   a &\\leq b    &&\\text{[por la hip\u00f3tesis 1 (\\(a \\leq b\\))]} \\\\
\n     &< c       &&\\text{[por la hip\u00f3tesis 2 (\\(b < c\\))]} \\\\\n     &\\leq d    &&\\text{[por la hip\u00f3tesis 3 (\\(c \\leq d\\))]} \\\\\n     &< e       &&\\text{[por la hip\u00f3tesis 4 (\\(d < e\\))]}\n\\end{align}\n\n2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
A partir de las hip\u00f3tesis 1 (\\(a \\leq b\\)) y 2 (\\(b < c\\)) se tiene\n\\[a < c\\]\nque, junto la hip\u00f3tesis 3 (\\(c \\leq d\\)) da\n\\[a < d\\]\nque, junto la hip\u00f3tesis 4 (\\(d < e\\)) da\n\\[a < e.\\]\n\n3\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Demostrar \\(a < e\\), por la hip\u00f3tesis 1 (\\(a \\leq b\\)) se reduce a\n\\[b < e\\]\nque, por la hip\u00f3tesis 2 (\\(b < c\\)), se reduce a\n\\[c < e\\]\nque, por la hip\u00f3tesis 3 (\\(c \\leq d\\)), se reduce a\n\\[d < e\\]\nque es cierto, por la hip\u00f3tesis 4.\n\nDemostraciones con Lean4<\/b><\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b c d e : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h1 : a \u2264 b)\r\n  (h2 : b < c)\r\n  (h3 : c \u2264 d)\r\n  (h4 : d < e) :\r\n  a < e :=\r\ncalc\r\n  a \u2264 b := h1\r\n  _ < c := h2\r\n  _ \u2264 d := h3\r\n  _ < e := h4\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h1 : a \u2264 b)\r\n  (h2 : b < c)\r\n  (h3 : c \u2264 d)\r\n  (h4 : d < e) :\r\n  a < e :=\r\nby\r\n  have h5 : a < c := lt_of_le_of_lt h1 h2\r\n  have h6 : a < d := lt_of_lt_of_le h5 h3\r\n  show a < e\r\n  exact lt_trans h6 h4\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h1 : a \u2264 b)\r\n  (h2 : b < c)\r\n  (h3 : c \u2264 d)\r\n  (h4 : d < e) :\r\n  a < e :=\r\nby\r\n  apply lt_of_le_of_lt h1\r\n  apply lt_trans h2\r\n  apply lt_of_le_of_lt h3\r\n  exact h4\r\n\r\n-- El desarrollo de la prueba es\r\n--\r\n--    a b c d e : \u211d,\r\n--    h1 : a \u2264 b,\r\n--    h2 : b < c,\r\n--    h3 : c \u2264 d,\r\n--    h4 : d < e\r\n--    \u22a2 a < e\r\n-- apply lt_of_le_of_lt h1,\r\n--    \u22a2 b < e\r\n-- apply lt_trans h2,\r\n--    \u22a2 c < e\r\n-- apply lt_of_le_of_lt h3,\r\n--    \u22a2 d < e\r\n-- exact h4,\r\n--    no goals\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h1 : a \u2264 b)\r\n  (h2 : b < c)\r\n  (h3 : c \u2264 d)\r\n  (h4 : d < e) :\r\n  a < e :=\r\nby linarith\r\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n