comp_hasFDerivWithinAt_iff — Mathlib

English

If iso is a linear isomorphism E ≃L[𝕜] F, the HasFDerivWithinAt of f ∘ iso with a derivative map equals the HasFDerivWithinAt of f with derivative map at iso x.

Русский

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

LaTeX

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

Lean4

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

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