English
For a linear equivalence L: G ≃L[𝕜] G' and f: E → (F →L[𝕜] G), the derivative within s satisfies fderivWithin 𝕜 (fun x ↦ L.toContinuousLinearMap.comp (f x)) s x = (((refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x).
Русский
Для линейного эквивалента L: G ≃L[𝕜] G' и отображения f: E → (F →L[𝕜] G) производная внутри s удовлетворяет равенству fderivWithin 𝕜 (λ x, L(x)) s x = (((refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x).
LaTeX
$$$fderivWithin 𝕜 (fun x \mapsto (L : G →L[𝕜] G').comp (f x)) s x = (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x)$$$
Lean4
theorem _root_.fderivWithin_continuousLinearEquiv_comp (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G))
(hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) s x =
(((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderivWithin 𝕜 f s x) :=
by
change fderivWithin 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x = _
rw [ContinuousLinearEquiv.comp_fderivWithin _ hs]
