strictAntiOn_derivWithin — Mathlib

English

If f is StrictConcaveOn on S and differentiableOn on S, then derivWithin f S is StrictAntiOn on S; i.e., it is strictly decreasing on S.

Русский

Если fStrictConcaveOn на S и дифференцируема на S, то derivWithin f S есть строгую антимонотонность на S; то есть строго убывает на S.

LaTeX

$$$\text{StrictConcaveOn}(\mathbb{R}, S, f)\land \text{DifferentiableOn}(\mathbb{R}, f, S)\Rightarrow \text{StrictAntiOn}(\operatorname{derivWithin} f\, S)\ S.$$$

Lean4

theorem strictAntiOn_derivWithin (hfc : StrictConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
    StrictAntiOn (derivWithin f S) S := by
  intro x hx y hy hxy
  exact (hfc.derivWithin_lt_slope hx hy hxy (hfd y hy)).trans (hfc.slope_lt_derivWithin hx hy hxy (hfd x hx))

Похожие утверждения