leftHomologyIso_hom_comp_homologyIso_inv

English

For h : S.LeftHomologyData, h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom.

Русский

Для h : S.LeftHomologyData выполняется h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom.

LaTeX

$$$h.leftHomologyIso.hom \circ h.homologyIso.inv = S.leftHomologyIso.hom$$$

Lean4

@[reassoc (attr := simp)]
theorem leftHomologyIso_hom_comp_homologyIso_inv (h : S.LeftHomologyData) :
    h.leftHomologyIso.hom ≫ h.homologyIso.inv = S.leftHomologyIso.hom :=
  by
  dsimp only [homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, Iso.hom_inv_id_assoc]

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