Si (∃z ∈ ℝ)[x < z < y], entonces x < y
Demostrar con Lean4 que si \((∃z ∈ ℝ)[x < z < y]\), entonces \(x < y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by sorry |
Demostración en lenguaje natural
Sea \(z\) tal que verifica las siguientes relaciones:
\begin{align}
x < z \tag{1} \\
z < y \tag{2}
\end{align}
Aplicando la propiedad transitiva a (1) y (2) se tiene que
\[ x < y \]
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 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) -- 1ª demostración -- =============== example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by rintro ⟨z, h1 : x < z, h2 : z < y⟩ show x < y exact lt_trans h1 h2 -- 2ª demostración -- =============== example : (∃ z : ℝ, x < z ∧ z < y) → x < y := by rintro ⟨z, h1, h2⟩ exact lt_trans h1 h2 -- 3ª demostración -- =============== example : (∃ z : ℝ, x < z ∧ z < y) → x < y := fun ⟨_, h1, h2⟩ ↦ lt_trans h1 h2 -- Lemas usados -- ============ -- variable (a b c : ℝ) -- #check (lt_trans : a < b → b < c → a < c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
