English
At a point x, the map x ↦ g(x)(f(x)) is differentiable provided g and f are differentiable at x.
Русский
В точке x отображение x ↦ g(x)(f(x)) дифференцируемо при условии дифференцируемости g и f в x.
LaTeX
$$$$MDifferentiableAt I 𝓘(𝕜, F_2) (\lambda x. g(x)(f(x))) x.$$$$
Lean4
/-- Applying a linear map to a vector is differentiable. Version in vector spaces. For a
version in nontrivial vector bundles, see `MDifferentiableAt.clm_apply_of_inCoordinates`. -/
theorem clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M} (hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x)
(hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x) : MDifferentiableAt I 𝓘(𝕜, F₂) (fun x => g x (f x)) x :=
DifferentiableWithinAt.comp_mdifferentiableWithinAt (t := univ) (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2)
(by
apply (Differentiable.differentiableAt _).differentiableWithinAt
exact differentiable_fst.clm_apply differentiable_snd)
(hg.prodMk_space hf) (by simp_rw [mapsTo_univ])
