map_succ'

Mathlib.Combinatorics.Additive.AP.Three.Behrend

URI: https://scilib.ai/kg/mathlib#Behrend.map_succ'

English

This is a variant: map(d)(a) = map(d)(a) with the tail expressed as a∘Fin.succ: map(d)(a) = a(0) + map(d)(a ∘ Fin.succ) · d.

Русский

Это вариант: map(d)(a) = a(0) + map(d)(a ∘ Fin.succ) · d.

LaTeX

$$$ map(d)(a) = a(0) + map(d)(a \\circ Fin.succ) \\cdot d $$$

Lean4

theorem map_succ' (a : Fin (n + 1) → ℕ) : map d a = a 0 + map d (a ∘ Fin.succ) * d :=
  map_succ _

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

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

Разделы

Аффилиация

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