Skip to main content

En ℝ, si y > x² entonces 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:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

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]} \newline &≥ 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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

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