English
Let iso be a linear isomorphism E ≃L[𝕜] F and f : F → G. Then HasFDerivWithinAt (f ∘ iso) f' s x is equivalent to HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).
Русский
Пусть iso — линейный изоморфизм E ≃L[𝕜] F и f : F → G. Тогда HasFDerivWithinAt (f ∘ iso) f' s x эквивалентно HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).
LaTeX
$$$ HasFDerivWithinAt (f \\circ iso) f' s x \\iff HasFDerivWithinAt f (f' \\circ iso.symm) s (iso x)$$$
Lean4
theorem comp_right_fderivWithin {f : F → G} {s : Set F} {x : E} (hxs : UniqueDiffWithinAt 𝕜 (iso ⁻¹' s) x) :
fderivWithin 𝕜 (f ∘ iso) (iso ⁻¹' s) x = (fderivWithin 𝕜 f s (iso x)).comp (iso : E →L[𝕜] F) :=
by
by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)
· exact (iso.comp_right_hasFDerivWithinAt_iff.2 h.hasFDerivWithinAt).fderivWithin hxs
· have : ¬DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x :=
by
intro h'
exact h (iso.comp_right_differentiableWithinAt_iff.1 h')
rw [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt this,
ContinuousLinearMap.zero_comp]
