trivializationOfMemPretrivializationAtlas

English

Promotion from a Pretrivialization in the atlas of a VectorPrebundle to a Trivialization exists, yielding a trivialization of the total space with the same base projection.

Русский

Существует переход от предтривиализации в атласе VectorPrebundle к тривиализации, дающий тривиализацию полного пространства с тем же отображением на базу.

LaTeX

$$$$ \\text{trivializationOfMemPretrivializationAtlas}(a,he) : \\text{Trivialization}$$$$

Lean4

/-- Promotion from a `Pretrivialization` in the `pretrivializationAtlas` of a
`VectorPrebundle` to a `Trivialization`. -/
def trivializationOfMemPretrivializationAtlas (a : VectorPrebundle R F E) {e : Pretrivialization F (π F E)}
    (he : e ∈ a.pretrivializationAtlas) : @Trivialization B F _ _ _ a.totalSpaceTopology (π F E) :=
  a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he

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