localTriv — Mathlib

English

For any index i, there is a natural local trivialization of the vector bundle constructed from the core, obtained from the corresponding fiber-bundle core trivialization.

Русский

Для любого индекса i существует естественная локальная тривиализация векторного расслоения, построенного из ядра, получаемая из тривиализации ядра фибер-бандла.

LaTeX

$$$\text{localTriv}(i) : \mathrm{Trivialization}(F, \pi F Z.\mathrm{Fiber})$$$

Lean4

/-- One of the standard local trivializations of a vector bundle constructed from core, taken by
considering this in particular as a fiber bundle constructed from core. -/
def localTriv (i : ι) : Trivialization F (π F Z.Fiber) :=
  Z.toFiberBundleCore.localTriv i

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