localTrivAt — Mathlib

English

The local trivialization at the index of b equals the specialized local triv at b.

Русский

Локальная тривиализация в точке b равна локальной тривиализации в позиции indexAt(b).

LaTeX

$$$Z.localTriv (Z.indexAt b) = Z.localTrivAt b$$$

Lean4

/-- Preferred local trivialization of a vector bundle constructed from core, at a given point, as
a bundle trivialization -/
def localTrivAt (b : B) : Trivialization F (π F Z.Fiber) :=
  Z.localTriv (Z.indexAt b)

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