blocksFun_mem_blocks

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.blocksFun_mem_blocks

English

For any i, blocksFun(i) is an element of the blocks of c.

Русский

Для любого i элемент blocksFun(i) принадлежит множеству blocks композиции.

LaTeX

$$$\\mathrm{blocksFun}(i) \\in \\mathrm{blocks}$$$

Lean4

@[simp]
theorem blocksFun_mem_blocks (i : Fin c.length) : c.blocksFun i ∈ c.blocks :=
  get_mem _ _

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

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

Разделы

Аффилиация

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