sizeUpTo_succ'

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.sizeUpTo_succ'

English

For i in Fin(c.length), sizeUpTo(i+1) = sizeUpTo(i) + blocksFun i.

Русский

Для i ∈ Fin(c.length) выполнено: sizeUpTo(i+1) = sizeUpTo(i) + blocksFun i.

LaTeX

$$$c.sizeUpTo((i : Fin c.length) + 1) = c.sizeUpTo(i) + c.blocksFun i$$$

Lean4

theorem sizeUpTo_succ' (i : Fin c.length) : c.sizeUpTo ((i : ℕ) + 1) = c.sizeUpTo i + c.blocksFun i :=
  c.sizeUpTo_succ i.2

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

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

Разделы

Аффилиация

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