English
Within-At differentiability of the map x ↦ g(x)(f(x)) when g and f are differentiable on a set s.
Русский
Within-At-дифференцируемость отображения x ↦ g(x)(f(x)) на множестве s.
LaTeX
$$$$MDifferentiableWithinAt I 𝓘(𝕜, F_2) (\lambda x. g(x)(f(x))) s x.$$$$
Lean4
/-- Applying a linear map to a vector is differentiable within a set. Version in vector spaces. For
a version in nontrivial vector bundles, see `MDifferentiableWithinAt.clm_apply_of_inCoordinates`. -/
theorem clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
(hg : MDifferentiableWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g s x) (hf : MDifferentiableWithinAt I 𝓘(𝕜, F₁) f s x) :
MDifferentiableWithinAt I 𝓘(𝕜, F₂) (fun x => g x (f x)) s 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])
