English
Let D be a convex subset of R. If f is continuous on D, differentiable on interior(D), and its derivative is nonnegative on interior(D), then f is nondecreasing on D.
Русский
Пусть D — выпуклое множество на R. Если f непрерывна на D, дифференцируема в interior(D) и производная неположительна на interior(D), тогда f возрастает (неубывает) на D.
LaTeX
$$$\forall x,y\in D,\; x \le y \Rightarrow f(x) \le f(y)$, under the condition that $0 \le f'(x)$ for all x in interior(D).$$
Lean4
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
`f` is a monotone function on `D`. -/
theorem monotoneOn_of_deriv_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) : MonotoneOn f D :=
fun x hx y hy hxy => by
simpa only [zero_mul, sub_nonneg] using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg x hx y hy hxy
