English
The direct product of two C^n vector bundles over the same base is a C^n vector bundle.
Русский
Переход координат в произведении гладок класса C^n.
LaTeX
$$$$\\text{ContMDiffVectorBundle } n (F_1 \\times F_2) (E_1 \\times^b E_2) IB$$$$
Lean4
/-- The direct sum of two `C^n` vector bundles over the same base is a `C^n` vector bundle. -/
instance contMDiffVectorBundle : ContMDiffVectorBundle n (F₁ × F₂) (E₁ ×ᵇ E₂) IB where
contMDiffOn_coordChangeL := by
rintro _ _ ⟨e₁, e₂, i₁, i₂, rfl⟩ ⟨e₁', e₂', i₁', i₂', rfl⟩
refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')
refine ContMDiffOn.clm_prodMap ?_ ?_
· refine (contMDiffOn_coordChangeL e₁ e₁').mono ?_
simp only [Trivialization.prod_baseSet, mfld_simps]
mfld_set_tac
· refine (contMDiffOn_coordChangeL e₂ e₂').mono ?_
simp only [Trivialization.prod_baseSet, mfld_simps]
mfld_set_tac
