comp_liftCycles — Mathlib

English

For α: A' ⟶ A, α ≫ S.liftCycles k hk = S.liftCycles (α ≫ k) with appropriate boundary adjustment.

Русский

Для стрелки α: A' ⟶ A выполняется равенство α ≫ S.liftCycles k hk = S.liftCycles (α ≫ k) c учетом границы.

LaTeX

$$$\alpha \;\circ S.liftCycles\,k\,hk = S.liftCycles(\alpha \circ k)$$$

Lean4

@[reassoc]
theorem comp_liftCycles {A' : C} (α : A' ⟶ A) :
    α ≫ S.liftCycles k hk = S.liftCycles (α ≫ k) (by rw [assoc, hk, comp_zero]) := by cat_disch

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