next_nat_succ

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#ChainComplex.next_nat_succ

English

For all i in natural numbers, next of (i+1) is i, as per the down-shape, i.e., next(i+1) = i.

Русский

Для всех i в натуральных числах, next(i+1) = i, согласно форме вниз.

LaTeX

$$$\forall i \in \mathbb{N},\; \text{next}_{\mathbb{N}}(i+1) = i$$$

Lean4

@[simp]
theorem next_nat_succ (i : ℕ) : (ComplexShape.down ℕ).next (i + 1) = i :=
  (ComplexShape.down ℕ).next_eq' rfl

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

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

Разделы

Аффилиация

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