comp_fderiv — Mathlib

English

Let iso be a linear isometry E ≃ F. Then fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F) ∘ (fderiv 𝕜 f x).

Русский

Пусть iso — линейная изометрия E ≃ F. Тогда fderiv 𝕜(iso ∘ f) x = (iso : E →L[𝕜] F) ∘ (fderiv 𝕜 f x).

LaTeX

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

Lean4

theorem comp_fderiv {f : G → E} {x : G} : fderiv 𝕜 (iso ∘ f) x = (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x) :=
  (iso : E ≃L[𝕜] F).comp_fderiv

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