π_comp_homologyIso_inv — Mathlib

English

For h : S.LeftHomologyData, the same relation h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ holds.

Русский

Для h : S.LeftHomologyData выполняется та же связь h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ.

LaTeX

$$$h.\pi \circ h.homologyIso.inv = h.cyclesIso.inv \circ S.homologyπ$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_homologyIso_inv (h : S.LeftHomologyData) : h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ :=
  by
  dsimp only [homologyπ, homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, π_comp_leftHomologyIso_inv_assoc]

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