transEquiv_transEquiv — Mathlib

English

Composition of transEquiv is associative: (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.transPartialEquiv f'').

Русский

Сложение через transEquiv два раза подряд образует ассоциативность: (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.transPartialEquiv f'')

LaTeX

$$$(e.transEquiv f').transEquiv f'' = e.transEquiv (f'.transPartialEquiv f'')$$$

Lean4

@[simp, mfld_simps]
theorem transEquiv_transEquiv (e : PartialEquiv α β) (f' : β ≃ γ) (f'' : γ ≃ δ) :
    (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'') := by
  simp only [transEquiv_eq_trans, trans_assoc, Equiv.trans_toPartialEquiv]

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