Existencia_de_valor_intermedio.md

Título	Autor
Hay algún número real entre 2 y 3	José A. Alonso

Demostrar con Lean4 que hay algún número real entre 2 y 3.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by sorry

Demostración en lenguaje natural

[mathjax] Puesto que \(2 < 5/2 < 3\), basta elegir \(5/2\).

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

-- 1ª demostración
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 :=
    by norm_num
  show ∃ x : ℝ, 2 < x ∧ x < 3
  exact Exists.intro (5 / 2) h

-- 2ª demostración
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 :=
    by norm_num
  show ∃ x : ℝ, 2 < x ∧ x < 3
  exact ⟨5 / 2, h⟩

-- 3ª demostración
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by
  use 5 / 2
  norm_num

-- 4ª demostración
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
⟨5 / 2, by norm_num⟩

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 28.