symm_trans_symm — Mathlib

English

The symmetric of the composition equals the reversed composition of symmetric components: (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv.

Русский

Симметричная композиции равна обращению композиции симметричных частей: (e^{-1} ∘ e' )^{-1} = (e'^{-1} ∘ e).

LaTeX

$$$(e.toPartialEquiv.symm.trans e'.toPartialEquiv).symm = e'.toPartialEquiv.symm.trans e.toPartialEquiv$$$

Lean4

theorem symm_trans_symm (e e' : Pretrivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).symm = e'.toPartialEquiv.symm.trans e.toPartialEquiv := by
  rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm]

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