fderiv — Mathlib

English

If iso is a linear isomorphism E ≃L[𝕜] F, then HasFDerivWithinAt (f ∘ iso) f' s x is equivalent to HasFDerivWithinAt f (f' ∘ iso.symm) s x at iso x.

Русский

Если iso — линейный изоморфизм E ≃L[𝕜] F, то HasFDerivWithinAt (f ∘ iso) f' s x эквивалентно HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).

LaTeX

$$$ HasFDerivWithinAt (f \\circ iso) f' s x \\iff HasFDerivWithinAt f (f' \\circ iso.symm) s (iso x)$$$

Lean4

protected theorem fderiv : fderiv 𝕜 iso x = iso :=
  iso.hasFDerivAt.fderiv

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