{x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y

Demostrar con Lean4 que
\[\{x ≤ y, y ≰ x\} ⊢ x ≤ y ∧ x ≠ y\]

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

Demostración en lenguaje natural

Como la conclusión es una conjunción, tenemos que desmostrar sus partes. La primera parte (\(x ≤ y\)) coincide con la hipótesis. Para demostrar la segunda parte (\(x ≠ y\)), supongamos que \(x = y\); entonces \(y ≤ x\) en contradicción con la segunda hipótesis.

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario