proj_eq — Mathlib

English

Let Z be the total space of a trivial fiber bundle over B with fiber F and projection proj: Z → B. Then there exists a homeomorphism e: Z ≃ B × F such that proj = fst ∘ e.

Русский

Пусть Z является общим пространством тривиального волокна над B с волокном F и требуется проекция proj: Z → B. Тогда существует гомеоморфизм e: Z ≃ B × F такой, что proj = fst ∘ e.

LaTeX

$$$\exists e: Z \cong B \times F,\ proj = \pi_1 \circ e$$$

Lean4

protected theorem proj_eq (h : IsHomeomorphicTrivialFiberBundle F proj) : ∃ e : Z ≃ₜ B × F, proj = Prod.fst ∘ e :=
  ⟨h.choose, (funext h.choose_spec).symm⟩

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