English
If a family of fiberwise linear morphisms depends smoothly on the base parameter, then the induced operation on the bundle of sections is contMDiff; the bundle-level composition is smooth in coordinates.
Русский
Если семейство линейных отображений вдоль волокон зависит плавно от параметра, то получаемая операция над секциями расслоения является ContMDiff; композиция в координатах тоже гладкая.
LaTeX
$$$\\text{ContMDiff} \\text{ clm bundle apply}$$$
Lean4
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`. -/
theorem clm_bundle_apply
(hϕ :
ContMDiff IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n
(fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂) (E := fun (x : B) ↦ (E₁ x →L[𝕜] E₂ x)) (b m) (ϕ m)))
(hv : ContMDiff IM (IB.prod 𝓘(𝕜, F₁)) n (fun m ↦ TotalSpace.mk' F₁ (b m) (v m))) :
ContMDiff IM (IB.prod 𝓘(𝕜, F₂)) n (fun m ↦ TotalSpace.mk' F₂ (b m) (ϕ m (v m))) := fun x ↦
(hϕ x).clm_bundle_apply (hv x)
