target_inter_preimage_symm_source_eq

English

The intersection of the target of a pretrivialization with the inverse image of the source under another pretrivialization equals the product of the intersection of the base sets with the universal fiber component.

Русский

Пересечение целевой области тривиализации с прообразом области определения под другой тривиализацией равно произведению пересечения базовых множеств на универсальный фактор.

LaTeX

$$$f.target\cap f.toPartialEquiv.symm^{-1}(e.source)=(e.baseSet\cap f.baseSet)\times\univ$$$

Lean4

theorem target_inter_preimage_symm_source_eq (e f : Pretrivialization F proj) :
    f.target ∩ f.toPartialEquiv.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ := by
  rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]

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