English
Let v: M → E1 and base b: M → B be differentiable, and let ϕ m: E1(b(m)) → E2(b(m)) depend smoothly on m. Then the map m ↦ ϕ(m)(v(m)) is differentiable in the sense of the bundle, i.e., the total space map m ↦ TotalSpace.mk'(F2, b(m), ϕ(m)(v(m))) is differentiable at the point.
Русский
Пусть v: M → E1 и база b: M → B дифференцируемы, а ϕ m: E1(b(m)) → E2(b(m)) зависят гладко от m. Тогда отображение m ↦ ϕ(m)(v(m)) дифференцируемо в смысле оболочки, то есть m ↦ TotalSpace.mk'(F2, b(m), ϕ(m)(v(m))) дифференцируемо в точке.
LaTeX
$$$$\text{MDifferentiableAt } IM (IB.\prod 𝓘(\mathbb{k}, F_1 \to_L F_2)) (m \mapsto \mathrm{TotalSpace.mk}' F_2 (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. -/
theorem clm_bundle_apply
(hϕ :
MDifferentiable 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)))
(hv : MDifferentiable IM (IB.prod 𝓘(𝕜, F₁)) (fun m ↦ TotalSpace.mk' F₁ (b m) (v m))) :
MDifferentiable IM (IB.prod 𝓘(𝕜, F₂)) (fun m ↦ TotalSpace.mk' F₂ (b m) (ϕ m (v m))) := fun x ↦
(hϕ x).clm_bundle_apply (hv x)
