of_dslope — Mathlib

English

For a function f, the dslope of the function x ↦ (x − a) f(x) at a equals the update of f at a by the derivative of x ↦ (x − a) f(x) at a.

Русский

Для функции f: dslope (x ↦ (x − a) f(x)) в точке a даёт обновленную функцию f в точке a с производной соответствующей функции.

LaTeX

$$$\text{dslope}( \lambda x. (x - a) \cdot f(x) )\ a = \text{update}\ f\ a \left( \mathrm{deriv}\left( \lambda x. (x - a) \cdot f(x) \right) a \right)$$$

Lean4

theorem of_dslope (h : DifferentiableOn 𝕜 (dslope f a) s) : DifferentiableOn 𝕜 f s := fun x hx => (h x hx).of_dslope

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