hasFDerivAt_zero — Mathlib

English

Let E and F be normed spaces over 𝕜 and x ∈ E. The Fréchet derivative at x of the constant zero map f: E → F is the zero linear map.

Русский

Пусть E и F — нормированные пространства над 𝕜 и x ∈ E. Производная по Фреше константного отображения f: E → F, f(y) = 0, в точке x равна нулевому линейному отображению.

LaTeX

$$$HasFDerivAt (0 : E \to F) (0 : E \toL[𝕜] F) x$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_zero (x : E) : HasFDerivAt (0 : E → F) (0 : E →L[𝕜] F) x :=
  hasFDerivAt_const _ _

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