vectorBundle — Mathlib

English

The tangent space carries a natural vector bundle structure with fiber E over M.

Русский

Касательное пространство обладает естественной структурой векторного расслоения с волокном E над M.

LaTeX

$$$$ \text{VectorBundle } \mathbb{K} E \, (\mathrm{TangentSpace} I) $$$$

Lean4

instance vectorBundle : VectorBundle 𝕜 E (TangentSpace I : M → Type _) :=
  (tangentBundleCore I M).vectorBundle

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