English
If g and f are differentiable withinAt, then the pointwise composition x ↦ g(x) ∘ f(x) is differentiable withinAt.
Русский
Если g и f дифференцируемы внутриAt, то композиция x ↦ g(x) ∘ f(x) дифференцируема внутриAt.
LaTeX
$$$$MDifferentiableWithinAt I 𝓘(𝕜, F_2 \to_L[𝕜] F_3) (\lambda x. g x \circ f x) s x.$$$$
Lean4
theorem clm_prodMap {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₁ × F₂ →L[𝕜] F₃ × F₄) (fun x => (g x).prodMap (f x)) s x :=
Differentiable.comp_mdifferentiableWithinAt (g := fun x : (F₁ →L[𝕜] F₃) × (F₂ →L[𝕜] F₄) => x.1.prodMap x.2) (f :=
fun x => (g x, f x)) (ContinuousLinearMap.prodMapL 𝕜 F₁ F₃ F₂ F₄).differentiable (hg.prodMk_space hf)
