comp_fderiv' — Mathlib

English

For maps f, the derivative of iso ∘ f is given pointwise by the same composition: fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F) ∘ (fderiv 𝕜 f x).

Русский

Для отображения f производная композиции iso ∘ f равна композиции изометрии с производной f: fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F) ∘ (fderiv 𝕜 f x).

LaTeX

$$$$ fderiv\\ 𝕜\\ (\\mathrm{iso} \\circ f) = x \\mapsto (\\mathrm{iso} : E \\to L[𝕜] F) .\\circ\\ (fderiv\\ 𝕜\\ f\\ x) $$$$

Lean4

theorem comp_fderiv' {f : G → E} : fderiv 𝕜 (iso ∘ f) = fun x ↦ (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x) :=
  by
  ext x : 1
  exact LinearIsometryEquiv.comp_fderiv iso

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