English
If g: M → F1 →L F3 and f: M → F2 →L F1 are ContMDiff, then x ↦ (g x).comp (f x) is ContMDiff.
Русский
Если g и f гладкие, то их композиция гладкая.
LaTeX
$$$\\forall x,\\ ContMDiffOn I (modelWithCornersSelf 𝕜 (ContinuousLinearMap (RingHom.id 𝕜) F_1 F_3)) n g x \\land \\ ContMDiffOn I (modelWithCornersSelf 𝕜 (ContinuousLinearMap (RingHom.id 𝕜) F_2 F_1)) n f x \\Rightarrow ContMDiffAt I (modelWithCornersSelf 𝕜 (ContinuousLinearMap (RingHom.id 𝕜) F_2 F_3)) n (fun x => (g x).comp (f x)) x.$$$
Lean4
/-- Applying a linear map to a vector is smooth. Version in vector spaces. For
versions in nontrivial vector bundles, see `ContMDiffAt.clm_apply_of_inCoordinates` and
`ContMDiffAt.clm_bundle_apply`. -/
nonrec theorem clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M} (hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x)
(hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x) : ContMDiffAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) x :=
hg.clm_apply hf
