one_le_blocksFun

Mathlib.Combinatorics.Enumerative.Composition

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

English

For any i, blocksFun(i) ≥ 1.

Русский

Для любого i: blocksFun(i) ≥ 1.

LaTeX

$$$1 \\le \\mathrm{blocksFun}(i)$$$

Lean4

@[simp]
theorem one_le_blocksFun (i : Fin c.length) : 1 ≤ c.blocksFun i :=
  c.one_le_blocks (c.blocksFun_mem_blocks i)

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

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

Разделы

Аффилиация

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