shiftFun_succ

Mathlib.AlgebraicTopology.ExtraDegeneracy

URI: https://scilib.ai/kg/mathlib#SSet.Augmented.StandardSimplex.shiftFun_succ

English

For i: Fin n, shiftFun f i.succ = f i.

Русский

Для i: Fin n выполнено shiftFun f i.succ = f i.

LaTeX

$$$ shiftFun(f)(i.succ) = f(i) $$$

Lean4

@[simp]
theorem shiftFun_succ {n : ℕ} {X : Type*} [Zero X] (f : Fin n → X) (i : Fin n) : shiftFun f i.succ = f i :=
  rfl

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

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

Разделы

Аффилиация

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