lt_slope_of_hasDerivWithinAt_Iio — Mathlib

English

If hfc is StrictConcaveOn on S, and hx, hy ∈ S with x < y, and HasDerivWithinAt f f' (Iio y) y, then f' < slope f x y.

Русский

Если fStricc ConcaveOn на S, x,y ∈ S с x < y, и HasDerivWithinAt f f' (Iio y) y выполняется, тогда f' < slope f x y.

LaTeX

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

Lean4

theorem lt_slope_of_hasDerivWithinAt_Iio (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' (Iio y) y) : f' < slope f x y := by
  simpa only [Pi.neg_def, slope_neg, neg_neg] using
    neg_lt_neg (hfc.neg.slope_lt_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

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