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:
1 2 3 4 |
import src.Funcion_no_acotada_superiormente example : ¬ acotadaSup (fun x ↦ x) := by sorry |
Read More «La función identidad no está acotada superiormente»