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
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.