(∃x ∈ ℝ)[2 < x < 3]
Demostrar con Lean4 que \((∃x ∈ ℝ)[2 < x < 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
Podemos usar el número \(\dfrac{5}{2}\) y comprobar que \(2 < \dfrac{5}{2} < 3\).
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 28 29 30 31 32 33 34 35 36 37 38 |
import Mathlib.Data.Real.Basic -- 1ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 show 2 < 5 / 2 ∧ 5 / 2 < 3 constructor . show 2 < 5 / 2 norm_num . show 5 / 2 < 3 norm_num -- 2ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 constructor . norm_num . norm_num -- 3ª demostración -- =============== example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 constructor <;> 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. 36.
