English
Let f: M → TotalSpace F E be differentiable within a set; then f is differentiable if and only if its base projection f(x).proj is differentiable and the fiber component given by the chosen trivialization is differentiable at the same point.
Русский
Пусть f: M → TotalSpace F E дифференцируема на множестве; тогда f дифференцируема тогда и только если проекция базы и волоконный компонент в тривиализации также дифференцируемы в той же точке.
LaTeX
$$$$MDifferentiableWithinAt IM (IB.\prod 𝓘(\mathbb{k}, F)) f s x \iff \Big( MDifferentiableWithinAt IM IB (\lambda x: f(x).proj) s x \ \wedge\ \ MDifferentiableWithinAt IM 𝓘(\mathbb{k}, F) (\lambda x: (\text{trivializationAt } F E (f x_0).proj (f x)).2) s x \Big).$$$$
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 within a set at a point. -/
theorem clm_bundle_apply₂
(hψ :
MDifferentiableWithinAt 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
x)
(hv : MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F₁)) (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s x)
(hw : MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F₂)) (fun m ↦ TotalSpace.mk' F₂ (b m) (w m)) s x) :
MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F₃)) (fun m ↦ TotalSpace.mk' F₃ (b m) (ψ m (v m) (w m))) s x :=
hψ.clm_bundle_apply hv |>.clm_bundle_apply hw
