blocks_length

Mathlib.Combinatorics.Enumerative.Composition

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

English

The length of the blocks list equals the number of blocks: |c.blocks| = l.

Русский

Длина списка блоков равна числу блоков: |c.blocks| = l.

LaTeX

$$$|c.blocks|=l,$$$

Lean4

@[simp]
theorem blocks_length : c.blocks.length = c.length :=
  length_ofFn

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

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

Разделы

Аффилиация

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