lt_slope_of_hasDerivAt — Mathlib

English

Let hfc be StrictConcaveOn on S. If hx ∈ S, hy ∈ S with x<y, Real f' is the derivative of f at y, then f' > slope f x y.

Русский

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

LaTeX

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

Lean4

theorem lt_slope_of_hasDerivAt (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
    (hf' : HasDerivAt f f' y) : f' < slope f x y :=
  hfc.lt_slope_of_hasDerivWithinAt_Iio hx hy hxy hf'.hasDerivWithinAt

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