image_preimage_eq_prod_univ — Mathlib

English

The image of the preimage of a base subset under the trivialization map equals the cartesian product with the universal fiber, i.e., e''(proj^{-1}(s)) = s × univ.

Русский

Образ предобраза proj^{-1}(s) через e даёт произведение s × univ.

LaTeX

$$$ e'' (proj^{-1}(s)) = s \times univ $$$

Lean4

theorem image_preimage_eq_prod_univ {s : Set B} (hb : s ⊆ e.baseSet) : e '' (proj ⁻¹' s) = s ×ˢ univ :=
  Subset.antisymm
    (image_subset_iff.mpr fun p hp => ⟨(e.proj_toFun p (e.preimage_subset_source hb hp)).symm ▸ hp, trivial⟩)
    fun p hp =>
    let hp' : p ∈ e.target := e.mem_target.mpr (hb hp.1)
    ⟨e.invFun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩

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