Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y
Demostrar con Lean4 que si \(x, y ∈ ℝ\) tales que \((∀ z)[y < z → x ≤ z]\), entonces \(x ≤ y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : ∀ z, y < z → x ≤ z) : x ≤ y := by sorry |
Read More «Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y"