En ℝ, y > x² ⊢ y > 0 ∨ y < -1
Demostrar con Lean4 que en \(ℝ\), \(y > x^2 ⊢ y > 0 ∨ y < -1\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : y > x^2) : y > 0 ∨ y < -1 := by sorry |
Demostración en lenguaje natural
Usando el lema
\[ (∀ x ∈ ℝ)[x² ≥ 0] \]
se tiene que
\begin{align}
y &> x² &&\text{[por hipótesis]} \\
&≥ 0 &&\text{[por el lema]}
\end{align}
Por tanto, \(y > 0\) y, al verificar la primera parte de la diyunción, se verifica la disyunción.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by have h1 : y > 0 := by calc y > x^2 := h _ ≥ 0 := pow_two_nonneg x show y > 0 ∨ y < -1 exact Or.inl h1 -- 2ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by left -- ⊢ y > 0 calc y > x^2 := h _ ≥ 0 := pow_two_nonneg x -- 3ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by left -- ⊢ y > 0 linarith [pow_two_nonneg x] -- 4ª demostración -- =============== example (h : y > x^2) : y > 0 ∨ y < -1 := by { left ; linarith [pow_two_nonneg x] } -- Lema usado -- ========== -- #check (pow_two_nonneg x : 0 ≤ x ^ 2) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 38.
