opcyclesMap_comp — Mathlib

English

Another presentation of the compatibility of opcyclesMap' with composition: opcyclesMap'(φ₁ ≫ φ₂) equals opcyclesMap' φ₁ followed by opcyclesMap' φ₂.

Русский

Ещё одно выражение совместимости opcyclesMap' с композицииφ₁ и φ₂.

LaTeX

$$$opcyclesMap' (φ_1 ≫ φ_2) h_1 h_3 = opcyclesMap' φ_1 h_1 h_2 ≫ opcyclesMap' φ_2 h_2 h_3$$$

Lean4

@[simp]
theorem opcyclesMap_comp [HasRightHomology S₁] [HasRightHomology S₂] [HasRightHomology S₃] (φ₁ : S₁ ⟶ S₂)
    (φ₂ : S₂ ⟶ S₃) : opcyclesMap (φ₁ ≫ φ₂) = opcyclesMap φ₁ ≫ opcyclesMap φ₂ :=
  opcyclesMap'_comp _ _ _ _ _

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