--- Título: Hay algún número real entre 2 y 3 Autor: 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.