toComposition_blocks

Mathlib.Combinatorics.Enumerative.Composition

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

English

The blocks of toCompositionAsSet(c) equal the function-derived list List.ofFn c.blocksFun.

Русский

Блоки toCompositionAsSet(c) равны списку List.ofFn c.blocksFun.

LaTeX

$$$c.toCompositionAsSet.blocks = List.ofFn c.blocksFun$$$

Lean4

@[simp]
theorem toComposition_blocks (c : CompositionAsSet n) : c.toComposition.blocks = c.blocks :=
  rfl

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

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

Разделы

Аффилиация

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