deriv_fderiv — Mathlib

English

For any f: 𝕜 → F and x, the deriv f x is obtained by applying the Frechet derivative to the unit input; more precisely, smulRight (1 : 𝕜 →L[𝕜] 𝕜) (deriv f x) = fderiv 𝕜 f x.

Русский

Для функции f: 𝕜 → F в точке x производная получается как применение Фрéше-дифференциала к единичному входу: smulRight(1)(deriv f x) = fderiv 𝕜 f x.

LaTeX

$$$$ \\operatorname{smulRight}(1 : 𝕜 \\toL[𝕜] 𝕜) (\\operatorname{deriv} f x) = fderiv 𝕜 f x $$$$

Lean4

theorem deriv_fderiv : smulRight (1 : 𝕜 →L[𝕜] 𝕜) (deriv f x) = fderiv 𝕜 f x := by
  simp only [deriv, ContinuousLinearMap.smulRight_one_one]

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