En ℝ, y > x² ⊢ y > 0 ∨ y < -1
Demostrar con Lean4 que en ℝ, y>x2⊢y>0∨y<−1.
Para ello, completar la siguiente teoría de Lean4:
Demostrar con Lean4 que en ℝ, y>x2⊢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 |