La función x ↦ -x no es monótona creciente
Demostrar con Lean4 que la función \(x ↦ -x\) no es monótona creciente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic import src.CNS_de_no_monotona example : ¬Monotone fun x : ℝ ↦ -x := by sorry |