derivWithin_lt_slope — Mathlib

English

Let hfc be StrictConcaveOn on S. If hx ∈ S, hy ∈ S with x<y, and DifferentiableWithinAt f S y, then derivWithin f S y < slope f x y.

Русский

Пусть fStrictConcaveOn на S. Если x,y ∈ S, x<y и DifferentiableWithinAt f S y, тогда derivWithin f S y < slope f x y.

LaTeX

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

Lean4

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

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