isHomeomorphicTrivialFiberBundle_snd

English

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

Русский

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

LaTeX

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

Lean4

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

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