English
The bundle-level differential properties of a vector bundle morphisms are compatible with the total space differentiability.
Русский
Дифференциальные свойства морфизмов векторных расслоений совместимы с дифференцируемостью общего пространства.
LaTeX
$$$\\text{contMDiffVectorBundle}$$$
Lean4
theorem mdifferentiableAt_hom_bundle (f : M → LE₁E₂) {x₀ : M} :
MDifferentiableAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) f x₀ ↔
MDifferentiableAt IM IB (fun x ↦ (f x).1) x₀ ∧
MDifferentiableAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂)
(fun x ↦ inCoordinates F₁ E₁ F₂ E₂ (f x₀).1 (f x).1 (f x₀).1 (f x).1 (f x).2) x₀ :=
mdifferentiableAt_totalSpace ..