sourceHomeomorphBaseSetProd — Mathlib

English

The source is homeomorphic to the product of the base set with the fiber.

Русский

Источник (источник тривиализации) гомоморфен произведению базового множества и волокна.

LaTeX

$$$ e.source \simeq_t e.baseSet \times F $$$

Lean4

/-- The source is homeomorphic to the product of the base set with the fiber. -/
def sourceHomeomorphBaseSetProd : e.source ≃ₜ e.baseSet × F :=
  (Homeomorph.setCongr e.source_eq).trans (e.preimageHomeomorph subset_rfl)

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