next_add

Mathlib.Algebra.Homology.ComplexShapeSigns

URI: https://scilib.ai/kg/mathlib#ComplexShape.next_add

English

The next-index operation interacts with H-addition: next(i1+i2) = next(i1) + i2 in the total framework.

Русский

Операция следующего индекса взаимодействует с операцией сложения: next(i1+i2) = next(i1) + i2.

LaTeX

$$$\\text{next}(i\\,+\\, j)=\\text{next}(i)+j$$$

Lean4

theorem next_add (p q : I) (hp : c.Rel p (c.next p)) : c.next (p + q) = c.next p + q :=
  c.next_eq' (c.rel_add hp q)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru