English
If g and f are differentiable (withinAt) as maps M → F1 →L F3 and M → F2 →L F1 respectively, then the pointwise product g(x) ∘ f(x) is differentiable within at.
Русский
Если g и f дифференцируемы как поочередно-образующиеся отображения, то их композиция x ↦ g(x) ∘ f(x) дифференцируема внутри множества.
LaTeX
$$$$\text{If } hg: MDifferentiableWithinAt I 𝓘(𝕜, F_1 \to_L[𝕜] F_3) g s x \text{ and } hf: MDifferentiableWithinAt I 𝓘(𝕜, F_2 \to_L[𝕜] F_1) f s x, \\ MDifferentiableWithinAt I 𝓘(𝕜, F_2 \to_L[𝕜] F_3) (\lambda x. g x ∘ f x) s x.$$$$
Lean4
theorem clm_comp {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M}
(hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) g s x) (hf : MDifferentiableWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) f s x) :
MDifferentiableWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) (fun x => (g x).comp (f x)) s x :=
Differentiable.comp_mdifferentiableWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₁) => x.1.comp x.2) (f :=
fun x => (g x, f x)) (differentiable_fst.clm_comp differentiable_snd) (hg.prodMk_space hf)
