Demostrar con Lean4 que en \u211d, si \(x \u2260 0\) entonces \(x < 0\) \u00f3 \(x > 0\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Data.Real.Basic\r\nvariable {x : \u211d}\r\n\r\nexample\r\n (h : x \u2260 0)\r\n : x < 0 \u2228 x > 0 :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Usando el siguiente lema
\n\[ (\u2200 x, y \u2208 \u211d)[x < y \u2228 x = y \u2228 y < x] \]
\nse demuestra distinguiendo tres casos.<\/p>\n
Caso 1: Supongamos que \(x < 0\). Entonces, se verifica la disyunci\u00f3n ya
\nque se verifica su primera parte.<\/p>\n
Caso 2: Supongamos que \(x = 0\). Entonces, se tiene una contradicci\u00f3n
\ncon la hip\u00f3tesis.<\/p>\n
Caso 3: Supongamos que \(x > 0\). Entonces, se verifica la disyunci\u00f3n ya
\nque se verifica su segunda parte.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Real.Basic\r\nvariable {x : \u211d}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : x \u2260 0)\r\n : x < 0 \u2228 x > 0 :=\r\nby\r\n rcases lt_trichotomy x 0 with hx1 | hx2 | hx3\r\n . -- hx1 : x < 0\r\n left\r\n -- \u22a2 x < 0\r\n exact hx1\r\n . -- hx2 : x = 0\r\n contradiction\r\n . -- hx3 : 0 < x\r\n right\r\n -- \u22a2 x > 0\r\n exact hx3\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : x \u2260 0)\r\n : x < 0 \u2228 x > 0 :=\r\nNe.lt_or_lt h\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : x \u2260 0)\r\n : x < 0 \u2228 x > 0 :=\r\nby aesop\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- variable (y : \u211d)\r\n-- #check (lt_trichotomy x y : x < y \u2228 x = y \u2228 y < 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