c — Mathlib · SciLib

English

The relation Rel in ComplexShape down ℕ is captured by the explicit mk relation ensuring the expected index-shifting property of the down-shape.

Русский

Отношение Rel в ComplexShape down ℕ задаётся явным mk-отношением, обеспечивая ожидаемое изменение индекса для понижающей формы.

LaTeX

$$$c.Rel(i,j) := \text{ComplexShape.down.mk}(i,j,h)$$$

Lean4

/-- As we are using chain complexes indexed by `ℕ`, we shall need the relation
`c` such `c m n` if and only if `n+1=m`. -/
abbrev c :=
  ComplexShape.down ℕ

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