isInducing_toProd — Mathlib

English

The total space of the trivial bundle is homeomorphic to the Cartesian product B × F via the natural isomorphism.

Русский

Полное пространство тривиального расслоения гомеоморфно произведению пространства оснований и волокна: B × F.

LaTeX

$$$ \mathrm{TotalSpace}\ F (\mathrm{Trivial}\ B F) \cong_t B \times F $$$

Lean4

theorem isInducing_toProd : IsInducing (TotalSpace.toProd B F) :=
  ⟨by simp only [instTopologicalSpaceProd, induced_inf, induced_compose]; rfl⟩

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