English
If a bundle morphism is mdifferentiable at a point, then the associated base projection and fiber coordinates are mdifferentiable at that point in their respective forms.
Русский
Если морфизм расслоения дифференцируем в точке, то базовая проекция и координаты волокна тоже дифференцируемы в этой точке.
LaTeX
$$$\\text{mdifferentiableAt}(f,x_0) \\iff \\text{mdifferentiableAt}(f.\\text{proj},x_0) \\land \\text{mdifferentiableAt}(inCoordinates, x_0)$$$
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 within a set at a point. -/
theorem clm_bundle_apply
(hϕ :
MDifferentiableWithinAt 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 x)
(hv : MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F₁)) (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) s x) :
MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F₂)) (fun m ↦ TotalSpace.mk' F₂ (b m) (ϕ m (v m))) s x :=
by
simp only [mdifferentiableWithinAt_hom_bundle] at hϕ
exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1
