Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona
Demostrar con Lean4 que si \(a, b ∈ ℝ\) tales que \(a ≤ b\) y \(f(b) < f(a)\), entonces \(f\) no es monótona
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable (a b : ℝ) example (h1 : a ≤ b) (h2 : f b < f a) : ¬ Monotone f := by sorry |
Read More «Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona"