homeomorphProd — Mathlib

English

There is a canonical homeomorphism between the total space of the trivial bundle and the product B × F, realized by the trivialization.

Русский

Существуют канонический гомеоморфизм между полным пространством тривиального расслоения и произведением B × F, реализованный тривиализацией.

LaTeX

$$$ \mathrm{Bundle.Trivial.trivialization} : \text{Trivialization } F (\pi F (Bundle.Trivial B F)) $$$

Lean4

/-- Homeomorphism between the total space of the trivial bundle and the Cartesian product. -/
@[simps!]
def homeomorphProd : TotalSpace F (Trivial B F) ≃ₜ B × F :=
  (TotalSpace.toProd _ _).toHomeomorphOfIsInducing (isInducing_toProd B F)

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