English
If g: M → F1 →L F3 and f: M → F2 →L F1 are ContMDiffAt, then x ↦ (g x).comp (f x) is ContMDiffAt.
Русский
Если g и f гладкие в точке, то их композиция гладкая в точке.
LaTeX
$$$\\text{If } hg : ContMDiffAt I 𝓘(𝕜, F_1 \\to_L F_3) n g x \\text{ and } hf : ContMDiffAt I 𝓘(𝕜, F_2 \\to_L F_1) n f x,\\ then\\ ContMDiffAt I 𝓘(𝕜, F_2 \\to_L F_3) n (fun x => (g x).comp (f x)) x.$$$
Lean4
/-- Applying a linear map to a vector is smooth within a set. Version in vector spaces. For
versions in nontrivial vector bundles, see `ContMDiffWithinAt.clm_apply_of_inCoordinates` and
`ContMDiffWithinAt.clm_bundle_apply`. -/
theorem clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {s : Set M} {x : M}
(hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x) (hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x) :
ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => g x (f x)) s x :=
ContDiffWithinAt.comp_contMDiffWithinAt (t := univ) (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2)
(by apply ContDiff.contDiffAt; exact contDiff_fst.clm_apply contDiff_snd) (hg.prodMk_space hf)
(by simp_rw [preimage_univ, subset_univ])
