English
Let M,B denote appropriate base spaces, and for each m ∈ M fix a linear map ϕ(m): E1(b(m)) → E2(b(m)) that depends smoothly on m, where b: M → B and v: M → E1(b(m)) is differentiable at x. Then the vector-valued map m ↦ ϕ(m)(v(m)) is differentiable at x as a section of the bundle over B; equivalently, the map m ↦ (b(m), ϕ(m)(v(m))) is differentiable at x.
Русский
Пусть M, B — подходящие базисные пространства, для каждого m ∈ M задано линейное отображение ϕ(m): E1(b(m)) → E2(b(m)) (зависит гладко от m), где b: M → B и v: M → E1(b(m)) дифференцируемы в точке x. Тогда отображение m ↦ ϕ(m)(v(m)) дифференцируемо в точке x как секция оболочки над B; эквивалентно, отображение m ↦ (b(m), ϕ(m)(v(m))) дифференцируемо в точке x.
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 at a point. -/
theorem clm_bundle_apply
(hϕ :
MDifferentiableAt 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)) x)
(hv : MDifferentiableAt IM (IB.prod 𝓘(𝕜, F₁)) (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) x) :
MDifferentiableAt IM (IB.prod 𝓘(𝕜, F₂)) (fun m ↦ TotalSpace.mk' F₂ (b m) (ϕ m (v m))) x :=
MDifferentiableWithinAt.clm_bundle_apply hϕ hv
