English
The trivial fiber bundle with base B and fiber F naturally carries a fiber-bundle structure, i.e., the projection map π: B × F → B makes B × F into a fiber bundle with fiber F.
Русский
Тривиальное фибровое расслоение с основанием B и фиброй F естественно имеет структуру фибрового расслоения: отображение π: B × F → B образует расслоение с волокном F.
LaTeX
$$$\mathrm{FiberBundle}(F,\ \mathrm{Bundle.Trivial}(B,F))$$$
Lean4
/-- Fiber bundle instance on the trivial bundle. -/
@[simps]
instance fiberBundle : FiberBundle F (Bundle.Trivial B F)
where
trivializationAtlas' := {trivialization B F}
trivializationAt' _ := trivialization B F
mem_baseSet_trivializationAt' := mem_univ
trivialization_mem_atlas' _ := mem_singleton _
totalSpaceMk_isInducing' _ := (homeomorphProd B F).symm.isInducing.comp (isInducing_const_prod.2 .id)
