English
If g is a continuous linear equivalence on the right, the iterated derivative of f ∘ g is the right composition with g of the iterated derivative of f.
Русский
Если g — непрерывная линейная эквивалентность справа, то итерационная производная от f ∘ g равна композиции справа с g применяемой к итеративной производной f.
LaTeX
$$$\forall f:\, E\to F,\; \text{cont diff right composition:}\ iteratedFDerivWithin 𝕜^i (f\circ g) (g^{-1}'s) x = (iteratedFDerivWithin 𝕜^i f s (g x)).compContinuousLinearMap (\,g\,)$$$
Lean4
/-- Composition by continuous linear equivs on the right respects higher differentiability at a
point. -/
theorem contDiffAt_comp_iff (e : G ≃L[𝕜] E) : ContDiffAt 𝕜 n (f ∘ e) (e.symm x) ↔ ContDiffAt 𝕜 n f x :=
by
rw [← contDiffWithinAt_univ, ← contDiffWithinAt_univ, ← preimage_univ]
exact e.contDiffWithinAt_comp_iff
