slope_lt_of_hasDerivWithinAt_Ioi — Mathlib

English

Let f be strictly concave on S. If x<y are in S and f is differentiable within at Ioi x, at the point x from the right, then the slope between x and y is strictly less than the right-derivative at x.

Русский

Пусть f строго вогнута на S. Если x<y в S и f дифференцируема в точке x слева или справа по границе Ioi x, то наклон секущей через x и y строго меньше правой производной в x.

LaTeX

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

Lean4

theorem slope_lt_of_hasDerivWithinAt_Ioi (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivWithinAt f f' (Ioi x) 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_Ioi hx hy hxy hf'.neg)

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