symm_trans_source_eq — Mathlib

English

The source of the symmetric-transformed pretrivialization equals the intersection product (baseSet ∩ baseSet') × univ.

Русский

Исходная область симместированного перехода равна пересечению оснований.

LaTeX

$$$(e.toPartialEquiv.symm.trans e'.toPartialEquiv).source=(e.baseSet\cap e'.baseSet)\times\univ$$$

Lean4

theorem symm_trans_source_eq (e e' : Pretrivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by
  rw [PartialEquiv.trans_source, e'.source_eq, PartialEquiv.symm_source, e.target_eq, inter_comm,
    e.preimage_symm_proj_inter, inter_comm]

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