En ℝ, -y > x² + 1 ⊢ y > 0 ∨ y < -1
Demostrar con Lean4 que en \(ℝ\),
\[ -y > x² + 1 ⊢ 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 + 1) : y > 0 ∨ y < -1 := by sorry |
Demostración en lenguaje natural
Usaremos los siguientes lemas
\begin{align}
&(∀ b, c ∈ ℝ)[b ≤ c → ∀ (a : ℝ), b + a ≤ c + a)] \tag{L1} \\
&(∀ a ∈ ℝ)[0 ≤ a²] \tag{L2} \\
&(∀ a ∈ ℝ)[0 + a = a] \tag{L3} \\
&(∀ a, b ∈ ℝ)[a < -b ↔ b < -a] \tag{L4}
\end{align}
Se tiene
\begin{align}
-y &> x^2 + 1 &&\text{[por la hipótesis]} \\
&≥ 0 + 1 &&\text{[por L1 y L2]} \\
&= 1 &&\text{[por L3]}
\end{align}
Por tanto,
\[ -y > 1 \]
y, aplicando el lema L4, se tiene
\[ y < -1 \]
Como se verifica la segunda parte de la disyunció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 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} -- 1ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by have h1 : -y > 1 := by calc -y > x^2 + 1 := by exact h _ ≥ 0 + 1 := add_le_add_right (pow_two_nonneg x) 1 _ = 1 := zero_add 1 have h2: y < -1 := lt_neg.mp h1 show y > 0 ∨ y < -1 exact Or.inr h2 -- 2ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by have h1 : -y > 1 := by linarith [pow_two_nonneg x] have h2: y < -1 := lt_neg.mp h1 show y > 0 ∨ y < -1 exact Or.inr h2 -- 3ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by have h1: y < -1 := by linarith [pow_two_nonneg x] show y > 0 ∨ y < -1 exact Or.inr h1 -- 4ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by right -- ⊢ y < -1 linarith [pow_two_nonneg x] -- 5ª demostración -- =============== example (h : -y > x^2 + 1) : y > 0 ∨ y < -1 := by { right ; linarith [pow_two_nonneg x] } -- Lemas usados -- ============ -- variable (a b c : ℝ) -- #check (add_le_add_right : b ≤ c → ∀ (a : ℝ), b + a ≤ c + a) -- #check (lt_neg : a < -b ↔ b < -a) -- #check (pow_two_nonneg a : 0 ≤ a ^ 2) -- #check (zero_add a : 0 + a = a) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 39.
