Demostrar con Lean4 que en \(\u211d\),
\n\[ -y > x\u00b2 + 1 \u22a2 y > 0 \u2228 y < -1 \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable {x y : \u211d}\n\nexample\n (h : -y > x^2 + 1)\n : y > 0 \u2228 y < -1 :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Usaremos los siguientes lemas
\n\begin{align}
\n &(\u2200 b, c \u2208 \u211d)[b \u2264 c \u2192 \u2200 (a : \u211d), b + a \u2264 c + a)] \tag{L1} \\
\n &(\u2200 a \u2208 \u211d)[0 \u2264 a\u00b2] \tag{L2} \\
\n &(\u2200 a \u2208 \u211d)[0 + a = a] \tag{L3} \\
\n &(\u2200 a, b \u2208 \u211d)[a < -b \u2194 b < -a] \tag{L4}
\n\end{align}<\/p>\n
Se tiene
\n\begin{align}
\n -y &> x^2 + 1 &&\text{[por la hip\u00f3tesis]} \\
\n &\u2265 0 + 1 &&\text{[por L1 y L2]} \\
\n &= 1 &&\text{[por L3]}
\n\end{align}
\nPor tanto,
\n\[ -y > 1 \]
\ny, aplicando el lema L4, se tiene
\n\[ y < -1 \]
\nComo se verifica la segunda parte de la disyunci\u00f3n, se verifica la disyunci\u00f3n.<\/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\n (h : -y > x^2 + 1)\n : y > 0 \u2228 y < -1 :=\nby\n have h1 : -y > 1 := by\n calc -y > x^2 + 1 := by exact h\n _ \u2265 0 + 1 := add_le_add_right (pow_two_nonneg x) 1\n _ = 1 := zero_add 1\n have h2: y < -1 := lt_neg.mp h1\n show y > 0 \u2228 y < -1\n exact Or.inr h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : -y > x^2 + 1)\n : y > 0 \u2228 y < -1 :=\nby\n have h1 : -y > 1 := by linarith [pow_two_nonneg x]\n have h2: y < -1 := lt_neg.mp h1\n show y > 0 \u2228 y < -1\n exact Or.inr h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : -y > x^2 + 1)\n : y > 0 \u2228 y < -1 :=\nby\n have h1: y < -1 := by linarith [pow_two_nonneg x]\n show y > 0 \u2228 y < -1\n exact Or.inr h1\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : -y > x^2 + 1)\n : y > 0 \u2228 y < -1 :=\nby\n right\n -- \u22a2 y < -1\n linarith [pow_two_nonneg x]\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : -y > x^2 + 1)\n : y > 0 \u2228 y < -1 :=\nby { right ; linarith [pow_two_nonneg x] }\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : \u211d)\n-- #check (add_le_add_right : b \u2264 c \u2192 \u2200 (a : \u211d), b + a \u2264 c + a)\n-- #check (lt_neg : a < -b \u2194 b < -a)\n-- #check (pow_two_nonneg a : 0 \u2264 a ^ 2)\n-- #check (zero_add a : 0 + a = a)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n