instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold

English

The chartAt map for the tangent bundle over model space is the identity on the canonical product model; i.e., tangentBundleModelSpaceChartAt.

Русский

Карта chartAt для касательного пространства над модельным пространством есть та же идентичность на каноническом произведении.

LaTeX

$$$\mathrm{tangentBundleModelSpaceChartAt} \; (p) = \mathrm{TotalProd}$$$

Lean4

instance [h : IsManifold I 2 M] : ContMDiffVectorBundle 1 E (TangentSpace I : M → Type _) I :=
  by
  have : IsManifold I (1 + 1) M := h
  exact TangentBundle.contMDiffVectorBundle

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