Demostrar con Lean4 que en \(\u211d\), si \(x < |y|\), entonces \(x < y\) \u00f3 \(x < -y\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample : x < |y| \u2192 x < y \u2228 x < -y :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Se demostrar\u00e1 por casos seg\u00fan \(y \u2265 0\).<\/p>\n
Primer caso: Supongamos que \(y \u2265 0\). Entonces, \(|y| = y\) y, por tanto, \(x < y\).<\/p>\n
Segundo caso: Supongamos que \(y < 0\). Entonces, \(|y| = -y\) y, por tanto, \(x < -y\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x < |y| \u2192 x < y \u2228 x < -y :=\nby\n intro h1\n -- h1 : x < |y|\n -- \u22a2 x < y \u2228 x < -y\n cases' le_or_gt 0 y with h2 h3\n . -- h2 : 0 \u2264 y\n left\n -- \u22a2 x < y\n rwa [abs_of_nonneg h2] at h1\n . -- h3 : 0 > y\n right\n -- \u22a2 x < -y\n rwa [abs_of_neg h3] at h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x < |y| \u2192 x < y \u2228 x < -y :=\nlt_abs.mp\n\n-- Lemas usados\n-- ============\n\n-- #check (le_or_gt x y : x \u2264 y \u2228 x > y)\n-- #check (abs_of_nonneg : 0 \u2264 x \u2192 abs x = x)\n-- #check (abs_of_neg : x < 0 \u2192 abs x = -x)\n-- #check (lt_abs : x < |y| \u2194 x < y \u2228 x < -y)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n