Demostrar con Lean4 que en \(\u211d\),
\n\[ |x + y| \u2264 |x| + |y| \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nvariable {x y : \u211d}\r\n\r\nexample : |x + y| \u2264 |x| + |y| :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Se usar\u00e1n los siguientes lemas
\n\begin{align}
\n &(\u2200 x \u2208 \u211d)[0 \u2264 x \u2192 |x| = x] \tag{L1} \\
\n &(\u2200 a, b, c, d \u2208 \u211d)[a \u2264 b \u2227 c \u2264 d \u2192 a + c \u2264 b + d] \tag{L2} \\
\n &(\u2200 x \u2208 \u211d)[x \u2264 |x|] \tag{L3} \\
\n &(\u2200 x \u2208 \u211d)[x < 0 \u2192 |x| = -x] \tag{L4} \\
\n &(\u2200 x, y \u2208 \u211d)[-(x + y) = -x + -y] \tag{L5} \\
\n &(\u2200 x \u2208 \u211d)[-x \u2264 |x|] \tag{L6}
\n\end{align}<\/p>\n
Se demostrar\u00e1 por casos seg\u00fan \(x + y \u2265 0\):<\/p>\n
Primer caso: Supongamos que \(x + y \u2265 0\). Entonces,
\n\begin{align}
\n |x + y| &= x + y &&\text{[por L1]} \\
\n &\u2264 |x| + |y| &&\text{[por L2 y L3]}
\n\end{align}<\/p>\n
Segundo caso: Supongamos que \(x + y < 0\). Entonces,
\n\begin{align}
\n |x + y| &= -(x + y) &&\text{[por L4]} \\
\n &= -x + -y &&\text{[por L5]} \\
\n &\u2264 |x| + |y| &&\text{[por L2 y L6]}
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\nvariable {x y : \u211d}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |x + y| \u2264 |x| + |y| :=\r\nby\r\n rcases le_or_gt 0 (x + y) with h1 | h2\r\n \u00b7 -- h1 : 0 \u2264 x + y\r\n show |x + y| \u2264 |x| + |y|\r\n calc |x + y| = x + y := by exact abs_of_nonneg h1\r\n _ \u2264 |x| + |y| := add_le_add (le_abs_self x) (le_abs_self y)\r\n . -- h2 : 0 > x + y\r\n show |x + y| \u2264 |x| + |y|\r\n calc |x + y| = -(x + y) := by exact abs_of_neg h2\r\n _ = -x + -y := by exact neg_add x y\r\n _ \u2264 |x| + |y| := add_le_add (neg_le_abs_self x) (neg_le_abs_self y)\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |x + y| \u2264 |x| + |y| := by\r\n rcases le_or_gt 0 (x + y) with h1 | h2\r\n \u00b7 -- h1 : 0 \u2264 x + y\r\n rw [abs_of_nonneg h1]\r\n -- \u22a2 x + y \u2264 |x| + |y|\r\n exact add_le_add (le_abs_self x) (le_abs_self y)\r\n . -- h2 : 0 > x + y\r\n rw [abs_of_neg h2]\r\n -- \u22a2 -(x + y) \u2264 |x| + |y|\r\n calc -(x + y) = -x + -y := by exact neg_add x y\r\n _ \u2264 |x| + |y| := add_le_add (neg_le_abs_self x) (neg_le_abs_self y)\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |x + y| \u2264 |x| + |y| := by\r\n rcases le_or_gt 0 (x + y) with h1 | h2\r\n \u00b7 -- h1 : 0 \u2264 x + y\r\n rw [abs_of_nonneg h1]\r\n -- \u22a2 x + y \u2264 |x| + |y|\r\n linarith [le_abs_self x, le_abs_self y]\r\n . -- h2 : 0 > x + y\r\n rw [abs_of_neg h2]\r\n -- \u22a2 -(x + y) \u2264 |x| + |y|\r\n linarith [neg_le_abs_self x, neg_le_abs_self y]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample : |x + y| \u2264 |x| + |y| :=\r\n abs_add x y\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (a b c d : \u211d)\r\n-- #check (abs_add x y : |x + y| \u2264 |x| + |y|)\r\n-- #check (abs_of_neg : x < 0 \u2192 |x| = -x)\r\n-- #check (abs_of_nonneg : 0 \u2264 x \u2192 |x| = x)\r\n-- #check (add_le_add : a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d)\r\n-- #check (le_abs_self a : a \u2264 |a|)\r\n-- #check (le_or_gt x y : x \u2264 y \u2228 x > y)\r\n-- #check (neg_add x y : -(x + y) = -x + -y)\r\n-- #check (neg_le_abs_self x : -x \u2264 |x|)\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