blocks_sum

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#CompositionAsSet.blocks_sum

← MathLib Explorer

English

The total sum of all block sizes equals n: b1 + ... + bl = n.

Русский

Сумма всех размеров блоков равна n: b1 + ... + bl = n.

LaTeX

$$$\\sum_{i=1}^l b_i = n$$$

Lean4

theorem blocks_sum : c.blocks.sum = n :=
  by
  have : c.blocks.take c.length = c.blocks := take_of_length_le (by simp [blocks])
  rw [← this, c.blocks_partial_sum c.length_lt_card_boundaries, c.boundary_length]
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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