English
Let hϕ and hv express differentiability at a point for a smoothly varying family of fiberwise linear maps ϕ m and a vector v m. Then the composite map m ↦ ϕ m(v m) is differentiable at that point as a section of the corresponding bundle over B.
Русский
Пусть hϕ и hv задают дифференцируемость в точке соответственно для гладко зависящей семейки линейных отображений ϕ m и вектора v m. Тогда композиция m ↦ ϕ m(v m) дифференцируема в точке как секция соответствующего расслоения над B.
LaTeX
$$$$\text{MDifferentiableAt } IM (IB.\prod 𝓘(\mathbb{k}, F)) (m \mapsto \mathrm{TotalSpace.mk}' F (b(m)) (\phi(m)(v(m)))) x.$$$$
Lean4
/-- Consider a differentiable 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 differentiable.
We give here a version of this statement on a set. -/
theorem clm_bundle_apply
(hϕ :
MDifferentiableOn IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂))
(fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂) (E := fun (x : B) ↦ (E₁ x →L[𝕜] E₂ x)) (b m) (ϕ m)) s)
(hv : MDifferentiableOn IM (IB.prod 𝓘(𝕜, F₁)) (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s) :
MDifferentiableOn IM (IB.prod 𝓘(𝕜, F₂)) (fun m ↦ TotalSpace.mk' F₂ (b m) (ϕ m (v m))) s := fun x hx ↦
(hϕ x hx).clm_bundle_apply (hv x hx)
