preimageHomeomorph — Mathlib

English

The preimage of a base subset under a trivialization is homeomorphic to the product of that base subset with the fiber.

Русский

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

LaTeX

$$$ e.preimageHomeomorph {s} (hb) : (proj^{-1} s).Elem \cong_t s.Elem \times F $$$

Lean4

/-- The preimage of a subset of the base set is homeomorphic to the product with the fiber. -/
def preimageHomeomorph {s : Set B} (hb : s ⊆ e.baseSet) : proj ⁻¹' s ≃ₜ s × F :=
  (e.toOpenPartialHomeomorph.homeomorphOfImageSubsetSource (e.preimage_subset_source hb)
        (e.image_preimage_eq_prod_univ hb)).trans
    ((Homeomorph.Set.prod s univ).trans ((Homeomorph.refl s).prodCongr (Homeomorph.Set.univ F)))

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