English
If f is continuous on a convex set D and differentiable on interior(D) with derivative nonpositive on interior(D), then f is antitone on D.
Русский
Если f непрерывна на выпуклом D и дифференцируема внутри interior(D) с производной неотрицательно не больше нуля, то f антимонотонна на D.
LaTeX
$$$\text{If } D \text{ convex}, \; f \text{ continuous on } D, \; f' \text{ within interior } D \le 0, \; \text{then } f \text{ is AntitoneOn } 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 nonpositive, then
`f` is an antitone function on `D`. -/
theorem antitoneOn_of_hasDerivWithinAt_nonpos {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, f' x ≤ 0) :
AntitoneOn f D :=
antitoneOn_of_deriv_nonpos hD hf (fun _ hx ↦ (hf' _ hx).differentiableWithinAt) fun x hx ↦ by
rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx
