comp_hasStrictFDerivAt_iff — Mathlib

English

If iso is a linear isomorphism E ≃L[𝕜] F, then HasStrictFDerivAt (f ∘ iso) ((f' ∘ iso) ) x iff HasStrictFDerivAt f f' (iso x).

Русский

Если iso — линейный изоморфизм, то HasStrictFDerivAt композицией сохраняется аналогично.

LaTeX

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

Lean4

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

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