symm_trans_target_eq — Mathlib

English

Similarly to the source, the target of the composed inverse transition equals (e.baseSet ∩ e'.baseSet) × univ. In symbols, (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) × univ.

Русский

Аналогично для области значения: целевая область перехода равна (e.baseSet ∩ e'.baseSet) × univ. То есть: (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.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' : Trivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ :=
  Pretrivialization.symm_trans_target_eq e.toPretrivialization e'

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