isHomeomorphicTrivialFiberBundle_fst

English

The first projection in a product is a trivial fiber bundle: the map fst: B × F → B yields a trivial fiber bundle with fiber F.

Русский

Первая проекция в произведении B × F → B образует тривиальный фибер-бандл с волокном F.

LaTeX

$$$\mathrm{IsHomeomorphicTrivialFiberBundle}(F,\mathrm{Prod.fst})$$$

Lean4

/-- The first projection in a product is a trivial fiber bundle. -/
theorem isHomeomorphicTrivialFiberBundle_fst : IsHomeomorphicTrivialFiberBundle F (Prod.fst : B × F → B) :=
  ⟨Homeomorph.refl _, fun _x => rfl⟩

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