instTopologicalSpacePullback — Mathlib

English

A trivial fiber bundle is homeomorphic to a product base × fiber, via a homeomorphism sending the projection to the first coordinate.

Русский

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

LaTeX

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

Lean4

instance [∀ x : B, TopologicalSpace (E x)] : ∀ x : B', TopologicalSpace ((f *ᵖ E) x) :=
  inferInstanceAs (∀ x, TopologicalSpace (E (f x)))

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