Demostrar con Lean4 que en \(\u211d\), \(y > x^2 \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)\n : y > 0 \u2228 y < -1 :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Usando el lema
\n\[ (\u2200 x \u2208 \u211d)[x\u00b2 \u2265 0] \]
\nse tiene que
\n\begin{align}
\n y &> x\u00b2 &&\text{[por hip\u00f3tesis]} \\
\n &\u2265 0 &&\text{[por el lema]}
\n\end{align}
\nPor tanto, \(y > 0\) y, al verificar la primera parte de la diyunci\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)\n : y > 0 \u2228 y < -1 :=\nby\n have h1 : y > 0 := by\n calc y > x^2 := h\n _ \u2265 0 := pow_two_nonneg x\n show y > 0 \u2228 y < -1\n exact Or.inl h1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : y > x^2)\n : y > 0 \u2228 y < -1 :=\nby\n left\n -- \u22a2 y > 0\n calc y > x^2 := h\n _ \u2265 0 := pow_two_nonneg x\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : y > x^2)\n : y > 0 \u2228 y < -1 :=\nby\n left\n -- \u22a2 y > 0\n linarith [pow_two_nonneg x]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : y > x^2)\n : y > 0 \u2228 y < -1 :=\nby { left ; linarith [pow_two_nonneg x] }\n\n-- Lema usado\n-- ==========\n\n-- #check (pow_two_nonneg x : 0 \u2264 x ^ 2)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n