fderivInnerCLM_apply — Mathlib

English

The derivative of the inner product bilinear map at p = (f,g) is the linear map (h,k) ↦ ⟪h, g⟫ + ⟪f, k⟫, i.e. fderivInnerCLM 𝕜 p = isBoundedBilinearMap_inner.deriv p.

Русский

Дифференциал билинейной карты ⟪f,g⟫ равен сумме частичных производных: при p=(f,g) производная по (h,k) равна ⟪h, g⟫ + ⟪f, k⟫.

LaTeX

$$$(f,g) \\mapsto \\langle f,g\\rangle\\text{ имеет производную } (h,k) \\mapsto \\langle h, g\\rangle + \\langle f, k\\rangle.$$$

Lean4

@[simp]
theorem fderivInnerCLM_apply (p x : E × E) : fderivInnerCLM 𝕜 p x = ⟪p.1, x.2⟫ + ⟪x.1, p.2⟫ :=
  rfl

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