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

Demostrar con Lean4 que. en , xyxyxyyx.

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

Demostración en lenguaje natural

Supongamos que
xyxy
Entonces, se tiene xy (por (1)) y, para probar yx, supongamos que
yx
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