English
For a morphism f: M → LE1E2, differentiability on a set s is equivalent to differentiability of the base part and the coordinates map on s, i.e., the total differentiability is determined by the base and coordinates parts.
Русский
Для отображения f: M → LE1E2, дифференциальность на множество s равносильна дифференцируемости базовой части и координатной карты на s.
LaTeX
$$$\\text{mdiffOn}(f,s) \\iff \\text{mdiffOn}(f|_{\\text{base}},s) \\land \\text{mdiffOn}(\\text{coordinates},s)$$$
Lean4
theorem contMDiffWithinAt_hom_bundle (f : M → LE₁E₂) {s : Set M} {x₀ : M} :
ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n f s x₀ ↔
ContMDiffWithinAt IM IB n (fun x ↦ (f x).1) s x₀ ∧
ContMDiffWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n
(fun x ↦ inCoordinates F₁ E₁ F₂ E₂ (f x₀).1 (f x).1 (f x₀).1 (f x).1 (f x).2) s x₀ :=
contMDiffWithinAt_totalSpace
