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. Demostración en lenguaje natural

Lo demostraremos por reducción al absurdo. Para ello, supongamos que
\[ x ≰ y \]
Entonces
\[ y < x \]
y, por la densidad de \(ℝ\), existe un \(a\) tal que
\[ y < a < x \]
Puesto que \(y < a\), por la hipótesis, se tiene que
\[ x ≤ a \]
en contradicción con
\[ a < x \]

2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Escribe un comentario