frontier_preimage — Mathlib

English

The frontier of the preimage of a base set under proj coincides with the preimage of the frontier in the base, intersected with the source of the trivialization.

Русский

Граница предобраза базового множества по proj совпадает с предобразом границы в основании, пересечённого с областью определения тривиализации.

LaTeX

$$$\\text{frontier}(\\text{preimage proj } s) = \\text{preimage proj } (\\text{frontier } s)$$$

Lean4

theorem frontier_preimage (e : Trivialization F proj) (s : Set B) :
    e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s) := by
  rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
    (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]

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