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 |