English
Let iso be a linear isomorphism between normed spaces E and F. Then a function f : F → G is differentiable on the whole domain if and only if f ∘ iso is differentiable on the corresponding domain, i.e., Differentiable 𝕜 (f ∘ iso) ↔ Differentiable 𝕜 f.
Русский
Пусть iso — линейное изоморфизм между евклидовыми пространствами E и F. Тогда функция f : F → G дифференцируема на всей области тогда и только тогда, когда композиция f ∘ iso дифференцируема на соответствующей области: Differentiable 𝕜 (f ∘ iso) ↔ Differentiable 𝕜 f.
LaTeX
$$$\\operatorname{Differentiable}_{\\mathbb{k}}(f \\circ iso) \\iff \\operatorname{Differentiable}_{\\mathbb{k}} f$$$
Lean4
theorem comp_right_differentiable_iff {f : F → G} : Differentiable 𝕜 (f ∘ iso) ↔ Differentiable 𝕜 f := by
simp only [← differentiableOn_univ, ← iso.comp_right_differentiableOn_iff, preimage_univ]
