--- Título: En ℝ, y > x^2 ⊢ y > 0 ∨ y < -1 Autor: José A. Alonso --- [mathjax] 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
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

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.