English
For two trivializations e and e', the domain of the composed inverse transition equals the intersection of their base sets, times all fiber data. In symbols, (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) × univ.
Русский
У двух тривиализаций e и e' область определения перехода-обратного отображения равна пересечению их базовых множеств, умноженному на всю фибру: (e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) × univ.
LaTeX
$$$ (e.toPartialEquiv.symm\,\text{trans}\, e'.toPartialEquiv).\text{source} = (e.baseSet \cap e'.baseSet) \times\mathrm{univ}.$$$
Lean4
theorem symm_trans_source_eq (e e' : Trivialization F proj) :
(e.toPartialEquiv.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ univ :=
Pretrivialization.symm_trans_source_eq e.toPretrivialization e'
