English
Let hϕ and hv be differentiable and set up that v is differentiable; then the map m ↦ TotalSpace.mk' F₂ (b(m)) (ϕ(m)(v(m))) is differentiable at x.
Русский
Пусть hϕ и hv дифференцируемы и v дифференцируема; тогда отображение m ↦ TotalSpace.mk' F₂ (b(m)) (ϕ(m)(v(m))) дифференцируемо в точке x.
LaTeX
$$$$\text{MDifferentiableAt } IM (IB.\prod 𝓘(\mathbb{k}, F_2)) (m \mapsto \mathrm{TotalSpace.mk}' F_2 (b(m)) (\phi(m)(v(m)))) x.$$$$
Lean4
/-- Consider differentiable maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ m` to `v m` and `w 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₂ →L[𝕜] F₃))
(fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (E := fun (x : B) ↦ (E₁ x →L[𝕜] 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)
(hw : MDifferentiableOn IM (IB.prod 𝓘(𝕜, F₂)) (fun m ↦ TotalSpace.mk' F₂ (b m) (w m)) s) :
MDifferentiableOn IM (IB.prod 𝓘(𝕜, F₃)) (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) s := fun x hx ↦
(hψ x hx).clm_bundle_apply₂ (hv x hx) (hw x hx)
