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:
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 |