English
Let iso be a linear isomorphism between normed spaces E and F. For any function f : F → G and any subset s ⊆ F, the differentiability of f on s is equivalent to the differentiability of f ∘ iso on the preimage iso^{-1}(s).
Русский
Пусть iso — линейное эквивалентное отображение между нормированными пространствами E и F. Для любой функции f : F → G и любой подмножества s ⊆ F равнозначна дифференцируемость f на s и дифференцируемость f ∘ iso на предобразе iso^{-1}(s).
LaTeX
$$$\\operatorname{DifferentiableOn}_{\\mathbb{k}}(f \\circ iso)(iso^{-1}(s)) \\iff \\operatorname{DifferentiableOn}_{\\mathbb{k}} f(s)$$$
Lean4
theorem comp_right_differentiableOn_iff {f : F → G} {s : Set F} :
DifferentiableOn 𝕜 (f ∘ iso) (iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s :=
by
refine ⟨fun H y hy => ?_, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩
rw [← iso.apply_symm_apply y, ← comp_right_differentiableWithinAt_iff]
apply H
simpa only [mem_preimage, apply_symm_apply] using hy
