contMDiffOn_coordChange — Mathlib

English

The direct sum of two C^n vector bundles over the same base is again a C^n vector bundle.

Русский

Прямой сумма двух расслоений сохраняет гладкость класса C^n.

LaTeX

$$$$\\text{ContMDiffVectorBundle } n (F_1 \\times F_2) (E_1 \\times^b E_2) IB$$$$

Lean4

theorem contMDiffOn_coordChange (IB : ModelWithCorners 𝕜 EB HB) [h : Z.IsContMDiff IB n] (i j : ι) :
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (Z.coordChange i j) (Z.baseSet i ∩ Z.baseSet j) :=
  h.1 i j

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