English
The total space projection maps a point in the total space to its base, respecting the fiber decomposition.
Русский
Проекция из полного пространства отображает точку в базовую точку, сохраняя разложение по фибрам.
LaTeX
$$$\mathrm{proj}: \text{TotalSpace } F E \to B$$$
Lean4
/-- The trivial vector bundle core, in which all the changes of coordinates are the
identity. -/
def trivialVectorBundleCore (ι : Type*) [Inhabited ι] : VectorBundleCore R B F ι
where
baseSet _ := univ
isOpen_baseSet _ := isOpen_univ
indexAt := default
mem_baseSet_at x := mem_univ x
coordChange _ _ _ := ContinuousLinearMap.id R F
coordChange_self _ _ _ _ := rfl
coordChange_comp _ _ _ _ _ _ := rfl
continuousOn_coordChange _ _ := continuousOn_const
