English
Let D be convex. If f is continuous on D and differentiable on interior(D) with f' nonnegative on interior(D), then f is monotone on D.
Русский
Пусть D выпукло. Если f непрерывна на D и дифференцируема внутри D, причём f' неотрицательна внутри D, то f монотонна на D.
LaTeX
$$$\forall x,y\in D,\; x \le y \Rightarrow f(x) \le f(y),$ given $0 \le f'(x)$ for all $x \in \operatorname{int}D$ and continuity/differentiability on 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_hasDerivWithinAt_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) (hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x) :
MonotoneOn f D :=
monotoneOn_of_deriv_nonneg hD hf (fun _ hx ↦ (hf' _ hx).differentiableWithinAt) fun x hx ↦ by
rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx
