slope_lt_deriv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem slope_lt_deriv (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hfd : DifferentiableAt ℝ f x) : slope f x y < deriv f x :=
  hfc.slope_lt_of_hasDerivAt hx hy hxy hfd.hasDerivAt

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