Si c es no negativo y f es monótona, entonces cf es monótona
Demostrar con Lean4 que si \(c\) es no negativo y \(f\) es monótona, entonces \(cf\) es monótona.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Real.Basic variable (f : ℝ → ℝ) variable {c : ℝ} example (mf : Monotone f) (nnc : 0 ≤ c) : Monotone (fun x ↦ c * f x) := by sorry |
Read More «Si c es no negativo y f es monótona, entonces cf es monótona»