toFiberBundle — Mathlib

English

From a VectorPrebundle, construct a FiberBundle structure on the same base and fiber type using the toFiberPrebundle data.

Русский

Из VectorPrebundle построить структуру FiberBundle на той же базовой области и типе волокна, используя данные toFiberPrebundle.

LaTeX

$$$$ toFiberBundle : @FiberBundle B F _ _ _ a.totalSpaceTopology _ $$$$

Lean4

/-- Make a `FiberBundle` from a `VectorPrebundle`; auxiliary construction for
`VectorPrebundle.toVectorBundle`. -/
def toFiberBundle : @FiberBundle B F _ _ _ a.totalSpaceTopology _ :=
  a.toFiberPrebundle.toFiberBundle

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