trans_transEquiv — Mathlib

English

Product-level compatibility: the following identity holds after translating by toPartialEquiv and trans:

Русский

Совместимость на уровне частичных эквивалентностей и соответствие через toPartialEquiv и trans:

LaTeX

$$$Eq\\left((e.trans e').transPartialEquiv f''\\right)\\left(e.transPartialEquiv (e'.transPartialEquiv f'' )\\right)$$$

Lean4

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

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