instContMDiffVectorBundle — Mathlib

English

For a VectorPrebundle with IsContMDiff, the selected contMDiffCoordChange map provides a C^n fiber coordinate change between two pretrivializations.

Русский

CoordChange гладок по волокнам.

LaTeX

$$$$\\text{contMDiffCoordChange}(n, IB, e, e')(b) : F \\to F$$$$

Lean4

/-- If a `VectorBundleCore` has the `IsContMDiff` mixin, then the vector bundle constructed from it
is a `C^n` vector bundle. -/
instance instContMDiffVectorBundle : ContMDiffVectorBundle n F Z.Fiber IB where
  contMDiffOn_coordChangeL := by
    rintro - - ⟨i, rfl⟩ ⟨i', rfl⟩
    refine (Z.contMDiffOn_coordChange IB i i').congr fun b hb ↦ ?_
    ext v
    exact Z.localTriv_coordChange_eq i i' hb v

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