Sean \\(a\\), \\(b\\) y \\(c\\) n\u00fameros reales. Demostrar con Lean4 que si \\(a \\leq b\\), entonces
\n\\[c – e^b \\leq c – e^a\\]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\n\r\nopen Real\r\n\r\nvariable (a b c : \u211d)\r\n\r\nexample\r\n (h : a \u2264 b)\r\n : c - exp b \u2264 c - exp a :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nAplicando la monoton\u00eda de la exponencial a la hip\u00f3tesis, se tiene
\n\\[e^a \\leq e^b\\]
\ny, restando de \\(c\\), se invierte la desigualdad
\n\\[c – e^b \u2264 c – e^a\\]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Analysis.SpecialFunctions.Log.Basic\r\n\r\nopen Real\r\n\r\nvariable (a b c : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (h : a \u2264 b)\r\n : c - exp b \u2264 c - exp a :=\r\nby\r\n have h1 : exp a \u2264 exp b :=\r\n exp_le_exp.mpr h\r\n show c - exp b \u2264 c - exp a\r\n exact sub_le_sub_left h1 c\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (h : a \u2264 b)\r\n : c - exp b \u2264 c - exp a :=\r\nby\r\n apply sub_le_sub_left _ c\r\n apply exp_le_exp.mpr h\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (h : a \u2264 b)\r\n : c - exp b \u2264 c - exp a :=\r\nsub_le_sub_left (exp_le_exp.mpr h) c\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample\r\n (h : a \u2264 b)\r\n : c - exp b \u2264 c - exp a :=\r\nby linarith [exp_le_exp.mpr 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