Demostrar con Lean4 que en \(\u211d\), \(x \u2264 |x|\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {x : \u211d}\n\nexample : x \u2264 |x| :=\nby sorry\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 x, y \u2208 \u211d)[x < y \u2192 x \u2264 y] \tag{L2} \\
\n &(\u2200 x \u2208 \u211d)[x \u2264 0 \u2192 x \u2264 -x] \tag{L3} \\
\n &(\u2200 x \u2208 \u211d)[x < 0 \u2192 |x| = -x] \tag{L4}
\n\end{align}<\/p>\n
Se demostrar\u00e1 por casos seg\u00fan \(x \u2265 0\):<\/p>\n
Primer caso: Supongamos que \(x \u2265 0\). Entonces,
\n\begin{align}
\n x &\u2264 x \\
\n &= |x| &&\text{[por L1]}
\n\end{align}<\/p>\n
Segundo caso: Supongamos que \(x < 0\). Entonces, por el L2, se tiene
\n\[ x \u2264 0 \tag{1} \]
\nPor tanto,
\n\begin{align}
\n x &\u2264 -x &&\text{[por L3 y (1)]} \\
\n &= |x| &&\text{[por L4]}
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\nvariable {x : \u211d}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\nby\n cases' le_or_gt 0 x with h1 h2\n . -- h1 : 0 \u2264 x\n show x \u2264 |x|\n calc x \u2264 x := le_refl x\n _ = |x| := (abs_of_nonneg h1).symm\n . -- h2 : 0 > x\n have h3 : x \u2264 0 := le_of_lt h2\n show x \u2264 |x|\n calc x \u2264 -x := le_neg_self_iff.mpr h3\n _ = |x| := (abs_of_neg h2).symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\nby\n cases' le_or_gt 0 x with h1 h2\n . -- h1 : 0 \u2264 x\n rw [abs_of_nonneg h1]\n . -- h2 : 0 > x\n rw [abs_of_neg h2]\n -- \u22a2 x \u2264 -x\n apply Left.self_le_neg\n -- \u22a2 x \u2264 0\n exact le_of_lt h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\nby\n rcases (le_or_gt 0 x) with h1 | h2\n . -- h1 : 0 \u2264 x\n rw [abs_of_nonneg h1]\n . -- h1 : 0 \u2264 x\n rw [abs_of_neg h2]\n linarith\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2264 |x| :=\n le_abs_self x\n\n-- Lemas usados\n-- ============\n\n-- variable (y : \u211d)\n-- #check (Left.self_le_neg : x \u2264 0 \u2192 x \u2264 -x)\n-- #check (abs_of_neg : x < 0 \u2192 |x| = -x)\n-- #check (abs_of_nonneg : 0 \u2264 x \u2192 |x| = x)\n-- #check (le_abs_self x : x \u2264 |x|)\n-- #check (le_neg_self_iff : x \u2264 -x \u2194 x \u2264 0)\n-- #check (le_of_lt : x < y \u2192 x \u2264 y)\n-- #check (le_or_gt x y : x \u2264 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