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