localTrivAt — Mathlib

English

A local trivialization at i yields a bundle trivialization of the projection π, with baseSet i and open source/target, compatible with the core data.

Русский

Локальная тривиализация при i задаёт тривиализацию биндела проекции π, с основанием baseSet i и открытыми областью источника/пунктов назначения, совместимую с данными ядра.

LaTeX

$$$\\text{localTrivAt}(i) :\\; \\text{Trivialization}(F, \\pi F Z.Fiber)$ with baseSet = Z.baseSet i, open_source = Z.open_source'(i).$$

Lean4

/-- Preferred local trivialization of a fiber 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)

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