Demostrar con Lean4 que si \\(a\\), \\(c\\), \\(d\\) y \\(f\\) son n\u00fameros reales tales que \\(d \u2264 f\\), entonces
\n\\[c + e^{a + d} \\leq c + e^{a + f}\\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\nopen Real\r\nvariable (a c d f : \u211d)\r\n\r\nexample\r\n (h : d \u2264 f)\r\n : c + exp (a + d) \u2264 c + exp (a + f) :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n\n
1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
De la hip\u00f3tesis, por la monotonia de la suma, se tiene
\n\\[a + d \\leq a + f\\]
\nque, por la monoton\u00eda de la exponencial, da
\n\\[e^{a + d} \\leq e^{a + f}\\]
\ny, por la monoton\u00eda de la suma, se tiene
\n\\[c + e^{a + d} \\leq c + e^{a + f}\\]<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Tenemos que demostrar que
\n\\[c + e^{a + d} \\leq c + e^{a + f}\\]
\nPor la monoton\u00eda de la suma, se reduce a
\n\\[e^{a + d} \\leq e^{a + f}\\]
\nque, por la monoton\u00eda de la exponencial, se reduce a
\n\\[a + d \\leq a + f\\]
\nque, por la monoton\u00eda de la suma, se reduce a
\n\\[d \\leq f\\]
\nque es la hip\u00f3tesis.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\nopen Real\r\nvariable (a c d f : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (h : d \u2264 f)\r\n : c + exp (a + d) \u2264 c + exp (a + f) :=\r\nby\r\n have h1 : a + d \u2264 a + f :=\r\n add_le_add_left h a\r\n have h2 : exp (a + d) \u2264 exp (a + f) :=\r\n exp_le_exp.mpr h1\r\n show c + exp (a + d) \u2264 c + exp (a + f)\r\n exact add_le_add_left h2 c\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (h : d \u2264 f)\r\n : c + exp (a + d) \u2264 c + exp (a + f) :=\r\nby\r\n apply add_le_add_left\r\n apply exp_le_exp.mpr\r\n apply add_le_add_left\r\n exact h\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