fderiv_deriv — Mathlib

English

Let 𝕜 be a nontrivially normed field and F a normed space. The derivative at x, viewed as a linear map, applied to the scalar 1, recovers the usual derivative: (fderiv 𝕜 f x : 𝕜 → F) 1 = deriv f x.

Русский

Пусть 𝕜 — ненулевое нормированное поле, F — нормированное пространство. Производная в точке x, рассматриваемая как линейное отображение, на входе 1 даёт обычную производную: (fderiv 𝕜 f x : 𝕜 → F) 1 = deriv f x.

LaTeX

$$$(fderiv 𝕜 f x : 𝕜 \\to F)(1) = \\operatorname{deriv} f x$$$

Lean4

theorem fderiv_deriv : (fderiv 𝕜 f x : 𝕜 → F) 1 = deriv f x :=
  rfl

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