contMDiffVectorBundle — Mathlib

English

The tangent bundle vector bundle structure is ContMDiff, i.e., the bundle has a ContMDiffVectorBundle structure.

Русский

Касательное расслоение является ContMDiff, то есть имеет конструкцию ContMDiffVectorBundle.

LaTeX

$$ContMDiffVectorBundle n E (TangentSpace I) I$$

Lean4

theorem contMDiffVectorBundle [h : IsManifold I (n + 1) M] :
    haveI : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
    ContMDiffVectorBundle n E (TangentSpace I : M → Type _) I :=
  by
  have : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
  have : (tangentBundleCore I M).IsContMDiff I n := tangentBundleCore.isContMDiff
  exact (tangentBundleCore I M).instContMDiffVectorBundle

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