symm_trans_target_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem symm_trans_target_eq (e e' : Pretrivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ := by
  rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]

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