En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x

Demostrar con Lean4 que. en \(ℝ\), \(x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x\).

Para ello, completar la siguiente teoría de Lean4:

Demostración en lenguaje natural

Supongamos que
\begin{align}
x ≤ y \tag{1} \\
x ≠ y \tag{2}
\end{align}
Entonces, se tiene \(x ≤ y\) (por (1)) y, para probar \(y ≰ x\), supongamos que
\[ y ≤ x \tag{3}\]
Aplicando la propiedad antimétrica a (1) y (3), se obtiene que \(x = y\), en contradicción con (2).

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario