asIsoHomologyι_inv_comp_homologyι

English

The inverse of the isomorphism from S.asIsoHomologyι composed with S.homologyι equals the identity.

Русский

Обратная часть изоморфизма S.asIsoHomologyι, умноженная на homologyι, даёт тождество.

LaTeX

$$(S.asIsoHomologyι hg).inv ≫ S.homologyι = 𝟙 _$$

Lean4

@[reassoc (attr := simp)]
theorem asIsoHomologyι_inv_comp_homologyι (hg : S.g = 0) [S.HasHomology] :
    (S.asIsoHomologyι hg).inv ≫ S.homologyι = 𝟙 _ :=
  Iso.inv_hom_id _

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