José A. AlonsoDemostrar que si f es monótona y c ≥ 0, entonces c·f es monótona.
Para ello, completar la siguiente teoría de Lean:
import data.real.basic variables (f : ℝ → ℝ) variable {c : ℝ} example (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := sorry |