English
If a family of linear maps f(y) differentiable at a point x yields a differentiable precomposition map, then the endpoint map y ↦ (f(y)).precomp F3 is differentiable at x.
Русский
Если семейство линейных отображений f(y) дифференциально в точке x, то отображение y ↦ (f(y)).precomp F3 дифференцируемо в точке x.
LaTeX
$$$\text{If } f: M \to (F_1 \to_L[\mathbb{K}] F_2) \text{ and } f \text{ is differentiable at } x, \, then \\ MDifferentiableAt \\ I \ 𝓘(\mathbb{K}, (F_2 \to_L[\mathbb{K}] F_3) \to_L[\mathbb{K}] (F_1 \to_L[\mathbb{K}] F_3)) (y \mapsto (f(y)).precomp F_3) x. $$$$
Lean4
nonrec theorem clm_precomp {f : M → F₁ →L[𝕜] F₂} {x : M} (hf : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) f x) :
MDifferentiableAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃))
(fun y ↦ (f y).precomp F₃ : M → (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) x :=
Differentiable.comp_mdifferentiableAt (ContinuousLinearMap.differentiable (ContinuousLinearMap.compL 𝕜 F₁ F₂ F₃).flip)
hf
