English
Let D be a convex subset of R. If f is continuous on D, differentiable on interior(D), and its HasDerivWithinAt on interior(D) is strictly negative, then f is strictly antitone on D.
Русский
Пусть D выпукло. Если f непрерывна на D, дифференцируема внутри interior(D), и производная внутри interior(D) строго отрицательна, то f строго антимонотонна на D.
LaTeX
$$$\text{If } D \text{ is convex } f \text{ continuous on } D, \; f \text{ differentiable on } \operatorname{int}D, \; \forall x \in \operatorname{int}D, \; f'(x) < 0, \; \text{then } f \text{ is antitone 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 strictly positive,
then `f` is a strictly monotone function on `D`. -/
theorem strictAntiOn_of_hasDerivWithinAt_neg {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) :
StrictAntiOn f D :=
strictAntiOn_of_deriv_neg hD hf fun x hx ↦ by rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx
