English
Let e be a continuous linear equivalence between G and E. Then for any set s ⊆ E and any function f: E → F, ContDiffOn 𝕜 n (f ∘ e) on e^{-1}(s) if and only if ContDiffOn 𝕜 n f on s.
Русский
Пусть e является непрерывной линейной эквивалентностью между G и E. Тогда для любого множества s ⊆ E и любой функции f: E → F выполняется: ContDiffOn 𝕜 n (f ∘ e) на e^{-1}(s) тогда и только тогда, когда ContDiffOn 𝕜 n f на s.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}\,^{n} (f \circ e)\,(e^{-1}(s)) \Longleftrightarrow \operatorname{ContDiffOn}_{\mathbb{K}}\,^{n} f\,s $$$
Lean4
/-- Composition by continuous linear equivs on the right respects higher differentiability on
domains. -/
theorem contDiffOn_comp_iff (e : G ≃L[𝕜] E) : ContDiffOn 𝕜 n (f ∘ e) (e ⁻¹' s) ↔ ContDiffOn 𝕜 n f s :=
⟨fun H => by simpa [Function.comp_def] using H.comp_continuousLinearMap (e.symm : E →L[𝕜] G), fun H =>
H.comp_continuousLinearMap (e : G →L[𝕜] E)⟩
