English
A continuation of the differentiability decomposition along a bundle morphism with base and fiber parts, showing equivalence to the conjunction of base differentiability and fiber coordinates differentiability.
Русский
Продолжение разложения по дифференцируемости вдоль морфизма расслоения — базовая часть иCoordinate часть.
LaTeX
$$$\\text{mdiffWithinAt}(f) \\iff \\text{mdiffWithinAt}(f.\\text{proj}) \\land \\text{mdiffWithinAt}(\\text{inCoordinates}(f))$$$
Lean4
theorem mdifferentiableWithinAt_hom_bundle (f : M → LE₁E₂) {s : Set M} {x₀ : M} :
MDifferentiableWithinAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) f s x₀ ↔
MDifferentiableWithinAt IM IB (fun x ↦ (f x).1) s x₀ ∧
MDifferentiableWithinAt 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) s x₀ :=
mdifferentiableWithinAt_totalSpace IB ..
