Demostrar con Lean4 que hay algún número real entre 2 y 3.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry |
Demostración en lenguaje natural
Puesto que 2<5/2<3, basta elegir 5/2.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 |
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
