contMDiffVectorBundle — Mathlib

English

A trivial vector bundle over a manifold is a C^n vector bundle.

Русский

Тривиальное расслоение гладко векторное.

LaTeX

$$$$\\text{contMDiffVectorBundle } n F (Bundle.Trivial B F) IB$$$$

Lean4

/-- A trivial vector bundle over a manifold is a `C^n` vector bundle. -/
instance contMDiffVectorBundle : ContMDiffVectorBundle n F (Bundle.Trivial B F) IB where
  contMDiffOn_coordChangeL := by
    intro e e' he he'
    obtain rfl := Bundle.Trivial.eq_trivialization B F e
    obtain rfl := Bundle.Trivial.eq_trivialization B F e'
    simp_rw [Bundle.Trivial.trivialization.coordChangeL]
    exact contMDiff_const.contMDiffOn

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