comp_right_fderiv — Mathlib

English

For a function f : F → G and iso: E ≃L[𝕜] F, HasFDerivAt (f ∘ iso) (f' ∘ iso) x holds if and only if HasFDerivAt f f' (iso x).

Русский

Для функции f : F → G и iso: E ≃L[𝕜] F верно HasFDerivAt (f ∘ iso) (f' ∘ iso) x ⇔ HasFDerivAt f f' (iso x).

LaTeX

$$$ HasFDerivAt (f \\circ iso) (f' \\circ iso) x \\iff HasFDerivAt f f' (iso x)$$$

Lean4

theorem comp_right_fderiv {f : F → G} {x : E} : fderiv 𝕜 (f ∘ iso) x = (fderiv 𝕜 f (iso x)).comp (iso : E →L[𝕜] F) :=
  by
  rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ]
  exact uniqueDiffWithinAt_univ

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