IsHomeomorphicTrivialFiberBundle — Mathlib

English

A trivial fiber bundle is homeomorphic to a product base × fiber via a homeomorphism that preserves projection as the first coordinate.

Русский

Тривиальное фибровое расслоение гомоморфно к произведению основания на фибру через гомоморфизм, сохраняющий проекцию как первую координату.

LaTeX

$$$\exists e: Z \cong_t B \times F,\forall x,\ (e x)_1 = \mathrm{proj}~x$$$

Lean4

/-- A trivial fiber bundle with fiber `F` over a base `B` is a space `Z`
projecting on `B` for which there exists a homeomorphism to `B × F` that sends `proj`
to `Prod.fst`. -/
def IsHomeomorphicTrivialFiberBundle (proj : Z → B) : Prop :=
  ∃ e : Z ≃ₜ B × F, ∀ x, (e x).1 = proj x

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