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]