English
Differentiability transfer under composition within s: if f is differentiable within s at x, then iso ∘ f has derivative iso ∘ (fderivWithin 𝕜 f s x).
Русский
Сохранение производной при композиции внутри области: если f дифференцируем внутри s в x, то произведение iso ∘ f имеет производную iso ∘ (fderivWithin 𝕜 f s x).
LaTeX
$$$fderivWithin 𝕜 (iso \circ f) s x = (iso : E →L[𝕜] F) \circ (fderivWithin 𝕜 f s x)$$$
Lean4
theorem comp_fderivWithin {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderivWithin 𝕜 f s x) :=
by
by_cases h : DifferentiableWithinAt 𝕜 f s x
· rw [fderiv_comp_fderivWithin x iso.differentiableAt h hxs, iso.fderiv]
· have : ¬DifferentiableWithinAt 𝕜 (iso ∘ f) s x := mt iso.comp_differentiableWithinAt_iff.1 h
rw [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt this,
ContinuousLinearMap.comp_zero]
