La función identidad no está acotada superiormente

Demostrar con Lean4 que la función identidad no está acotada superiormente.

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

Demostración en lenguaje natural


Usando el lema de ejercicio anterior (que afirma que si para cada a, existe un x tal que f(x)>a, entonces f no tiene cota superior) basta demostrar que
(a)(x)[x>a]
Sea a. Entonces a+1>a y, por tanto, (x)[x>a].

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario