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 |
Demostración en lenguaje natural
Usando el lema del ejercicio anterior que afirma que una función f no es monótona syss existen x e y tales que x ≤ y y f(x) > f(y), basta demostrar que
\[ (∃ x, y)[x ≤ y ∧ -x > -y] \]
Basta elegir 2 y 3 ya que
\[ 2 ≤ 3 ∧ -2 > -3 \]
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Real.Basic import src.CNS_de_no_monotona example : ¬Monotone fun x : ℝ ↦ -x := by apply not_Monotone_iff.mpr -- ⊢ ∃ x y, x ≤ y ∧ -x > -y use 2, 3 -- ⊢ 2 ≤ 3 ∧ -2 > -3 norm_num |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 37.
