homologyIso_hom_comp_rightHomologyIso_inv

English

For h : S.RightHomologyData, the equation h.homologyIso.inv ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv holds.

Русский

Для h : S.RightHomologyData выполняется h.homologyIso.inv ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv.

LaTeX

$$$h.homologyIso.inv \circ h.rightHomologyIso.inv = S.rightHomologyIso.inv$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyIso_hom_comp_rightHomologyIso_inv (h : S.RightHomologyData) :
    h.homologyIso.hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv :=
  by
  dsimp only [homologyIso]
  simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id, comp_id]

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