Demostrar con Lean4 que si \\(a\\), \\(b\\) y \\(c\\) son n\u00fameros reales tales que \\(2a \\leq 3b\\), \\(1 \\leq a\\) y \\(c = 2\\), entonces \\(c + a \\leq 5b\\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b c : \u211d)\r\n\r\nexample\r\n (h1 : 2 * a \u2264 3 * b)\r\n (h2 : 1 \u2264 a)\r\n (h3 : c = 2)\r\n : c + a \u2264 5 * b :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la siguiente cadena de desigualdades
\n\\begin{align}
\n c + a &= 2 + a &&\\text{[por la hip\u00f3tesis 3 (\\(c = 2\\))]} \\\\
\n &\\leq 2\u00b7a + a &&\\text{[por la hip\u00f3tesis 2 (\\(1 \\leq a\\))]} \\\\
\n &= 3\u00b7a \\\\
\n &\\leq 9\/2\u00b7b &&\\text{[por la hip\u00f3tesis 1 (\\(2\u00b7a \\leq 3\u00b7b\\))]} \\\\
\n &\\leq 5\u00b7b
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b c : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (h1 : 2 * a \u2264 3 * b)\r\n (h2 : 1 \u2264 a)\r\n (h3 : c = 2)\r\n : c + a \u2264 5 * b :=\r\ncalc\r\n c + a = 2 + a := by rw [h3]\r\n _ \u2264 2 * a + a := by linarith only [h2]\r\n _ = 3 * a := by linarith only []\r\n _ \u2264 9\/2 * b := by linarith only [h1]\r\n _ \u2264 5 * b := by linarith\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (h1 : 2 * a \u2264 3 * b)\r\n (h2 : 1 \u2264 a)\r\n (h3 : c = 2)\r\n : c + a \u2264 5 * b :=\r\nby linarith\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