fderiv_const_apply — Mathlib

English

Let f: E → F be the constant map f(y) = c. Then its Fréchet derivative at every point x is the zero linear map.

Русский

Пусть f: E → F будет константной картой f(y) = c. Тогда производная Фреше в любой точке x равна нулевой линейной карте.

LaTeX

$$$\mathrm{fderiv}_{\mathbb{k}}(\lambda y: E.\, c) = 0$$$

Lean4

theorem fderiv_const_apply (c : F) : fderiv 𝕜 (fun _ => c) x = 0 :=
  (hasFDerivAt_const c x).fderiv

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