comp_hasFDerivAt_iff — Mathlib

English

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

Русский

Если iso — линейный изоморфизм, то 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

theorem comp_hasFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasFDerivAt f f' x :=
  (iso : E ≃L[𝕜] F).comp_hasFDerivAt_iff

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