prev_nat_succ

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.prev_nat_succ

English

For any i in ℕ, prev of (i+1) equals i in the up-shape: prev(i+1) = i.

Русский

Для любого i ∈ ℕ, prev(i+1) = i в форме вверх.

LaTeX

$$$\text{prev}_{\text{up}}(i+1) = i$$$

Lean4

@[simp]
theorem prev_nat_succ (i : ℕ) : (ComplexShape.up ℕ).prev (i + 1) = i :=
  (ComplexShape.up ℕ).prev_eq' rfl

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

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

Разделы

Аффилиация

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