slope_lt_of_hasDerivWithinAt — Mathlib

English

Let hfc be StrictConcaveOn on S. If hx, hy ∈ S with x<y and f is differentiableWithinAt f on S at x, then slope f x y < f' where f' is the derivative within at x.

Русский

Пусть hfc — StrictConcaveOn на S. Пусть x,y∈S и x<y, и f дифференцируема внутри S в точке x; тогда slope f x y < f', где f' — производная внутри S в x.

LaTeX

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

Lean4

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

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