fderiv — Mathlib

English

The derivative of a continuous affine map f at any x equals its linear part, f.contLinear.

Русский

Производная непрерывного аффинного отображения f в любой точке x равна его линейной части f.contLinear.

LaTeX

$$$ fderiv_{\mathbb{k}}(f)(x) = f.contLinear. $$$

Lean4

@[simp]
theorem fderiv (f : V →ᴬ[𝕜] W) {x : V} : fderiv 𝕜 f x = f.contLinear :=
  by
  conv_lhs => rw [f.decomp]
  rw [fderiv_add f.contLinear.differentiableAt]; swap
  · exact differentiableAt_const _
  simp only [fderiv_const, Pi.zero_apply, add_zero, ContinuousLinearMap.fderiv]

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