English
If f: M → F1 →L[𝕜] F2 is differentiable on a set s in the sense of WithinAt, then the map y ↦ (f y).precomp F3 is differentiable on s in the corresponding sense for the target space of functions.
Русский
Если f: M → F1 →L[𝕜] F2 дифференцируема на множестве s во внутреннем смысле, то отображение y ↦ (f y).precomp F3 дифференцируемо на s в соответствующем смысле для целевого пространства функций.
LaTeX
$$$$\forall s\subseteq M, \ x\in M \,:\\ MDifferentiableWithinAt \\ I \\ 𝓘(𝕜, F_1 \to_L F_2) f s x \Rightarrow \\ MDifferentiableWithinAt \\ I \\ 𝓘(𝕜, (F_2 \to_L F_3) \to_L (F_1 \to_L F_3)) (\lambda y. (f(y)).precomp F_3) s x. $$$$
Lean4
theorem clm_precomp {f : M → F₁ →L[𝕜] F₂} {s : Set M} (hf : MDifferentiableOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) f s) :
MDifferentiableOn I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃))
(fun y ↦ (f y).precomp F₃ : M → (F₂ →L[𝕜] F₃) →L[𝕜] (F₁ →L[𝕜] F₃)) s :=
fun x hx ↦ (hf x hx).clm_precomp
