mdifferentiableAt_hom_bundle — Mathlib

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 ..

Похожие утверждения