Demostrar con Lean4 que \\(a\\), \\(b\\), \\(c\\), \\(d\\) y \\(f\\) son n\u00fameros reales tales que \\(a \\leq b\\) y \\(c < d\\), entonces\n\\[a + e^c + f \\leq b + e^d + f\\]\n\nPara ello, completar la siguiente teor\u00eda de Lean4:\n\n\n\n
\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\nopen Real\r\nvariable (a b c d f : \u211d)\r\n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : c < d)\r\n : a + exp c + f < b + exp d + f :=\r\nby sorry\r\n<\/pre>\n<\/p>\n\n
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n
1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Aplicando a la hip\u00f3tesis 3 (\\(c < d\\)) la monoton\u00eda de la exponencial, se tiene\n\\[e^c < e^d\\]\nque, junto a la hip\u00f3tesis 1 (\\(a \\leq b\\)) y la monoton\u00eda de la suma da\n\\[a + e^c < b + e^d\\]\ny, de nuevo por la monoton\u00eda de la suma, se tiene\n\\[a + e^c + f < b + e^d + f\\]\n\n2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Tenemos que demostrar que
\n\\[(a + e^c) + f < (b + e^d) + f\\]\nque, por la monoton\u00eda de la suma, se reduce a las siguientes dos desigualdades:\n\\begin{align}\n &a + e^c < b + e^d \\tag{1} \\\\\n &f \\leq f \\tag{2}\n\\end{align}\n\nLa (1), de nuevo por la monoton\u00eda de la suma, se reduce a las siguientes dos:\n\\begin{align}\n &a \\leq b \\tag{1.1} \\\\\n &e^c < e^d \\tag{1.2}\n\\end{align}\n\n\n\n
La (1.1) se tiene por la hip\u00f3tesis 1, la (1.2) se tiene aplicando la monoton\u00eda de la exponencial a la hip\u00f3tesis 2 y la (2) se tiene por la propiedad reflexiva.<\/p>\nDemostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\nopen Real\r\nvariable (a b c d f : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : c < d)\r\n : a + exp c + f < b + exp d + f :=\r\nby\r\n have h3 : exp c < exp d :=\r\n exp_lt_exp.mpr h2\r\n have h4 : a + exp c < b + exp d :=\r\n add_lt_add_of_le_of_lt h1 h3\r\n show a + exp c + f < b + exp d + f\r\n exact add_lt_add_right h4 f\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : c < d)\r\n : a + exp c + f < b + exp d + f :=\r\nby\r\n apply add_lt_add_of_lt_of_le\r\n { apply add_lt_add_of_le_of_lt\r\n { exact h1 }\r\n { apply exp_lt_exp.mpr\r\n exact h2 } }\r\n { apply le_refl }\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (h1 : a \u2264 b)\r\n (h2 : c < d)\r\n : a + exp c + f < b + exp d + f :=\r\nby\r\n apply add_lt_add_of_lt_of_le\r\n . apply add_lt_add_of_le_of_lt h1\r\n apply exp_lt_exp.mpr h2\r\n rfl\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n