slope_lt_derivWithin — Mathlib

English

If hfc is StrictConcaveOn on S and hx, hy ∈ S with x<y, and f is differentiableWithinAt on S at y, then slope f x y < derivWithin f S x.

Русский

Если hfc — StrictConcaveOn на S и x,y ∈ S, x<y, и f дифференцируема внутри S в y, то slope f x y < derivWithin f S x.

LaTeX

$$$\text{StrictConcaveOn}(\mathbb{R}, S, f)\land hx\in S\land hy\in S\land x

Lean4

theorem slope_lt_derivWithin (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableWithinAt ℝ f S x) : slope f x y < derivWithin f S x :=
  hfc.slope_lt_of_hasDerivWithinAt hx hy hxy hfd.hasDerivWithinAt

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