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