Demostrar con Lean4 que si \\(a\\) y \\(b\\) n\u00fameros reales, entonces
\n\\[|a| – |b| \\leq |a – b|\\]<\/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 : \u211d)\r\n\r\nexample : |a| - |b| \u2264 |a - b| :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraciones en lenguaje natural (LN)<\/b><\/p>\n
\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la siguiente cadena de desigualdades
\n\\begin{align}
\n |a| – |b| &= |a – b + b| – |b| \\\\
\n &\\leq (|a – b| + |b|) – |b| &&\\text{[por la desigualdad triangular]}\\\\
\n &= |a – b|
\n\\end{align}<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Por la desigualdad triangular
\n\\[ |a – b + b| \\leq |a – b| + |b| \\]
\nsimplificando en la izquierda
\n\\[ |a| \\leq |a – b| + |b| \\]
\ny, pasando \\(|b|\\) a la izquierda
\n\\[ |a| – |b| \u2264 |a – b| \\]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\n\r\nvariable (a b : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\r\nexample : |a| - |b| \u2264 |a - b| :=\r\ncalc |a| - |b|\r\n = |a - b + b| - |b| :=\r\n congrArg (fun x => |x| - |b|) (sub_add_cancel a b).symm\r\n _ \u2264 (|a - b| + |b|) - |b| :=\r\n sub_le_sub_right (abs_add (a - b) b) (|b|)\r\n _ = |a - b| :=\r\n add_sub_cancel (|a - b|) (|b|)\r\n\r\n-- 2\u00aa demostraci\u00f3n (basada en la 1\u00aa en LN)\r\nexample : |a| - |b| \u2264 |a - b| :=\r\ncalc |a| - |b|\r\n = |a - b + b| - |b| := by\r\n rw [sub_add_cancel]\r\n _ \u2264 (|a - b| + |b|) - |b| := by\r\n apply sub_le_sub_right\r\n apply abs_add\r\n _ = |a - b| := by\r\n rw [add_sub_cancel]\r\n\r\n-- 3\u00aa demostraci\u00f3n (basada en la 2\u00aa en LN)\r\nexample : |a| - |b| \u2264 |a - b| :=\r\nby\r\n have h1 : |a - b + b| \u2264 |a - b| + |b| := abs_add (a - b) b\r\n rw [sub_add_cancel] at h1\r\n exact abs_sub_abs_le_abs_sub a b\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : |a| - |b| \u2264 |a - b| :=\r\nabs_sub_abs_le_abs_sub a b\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