one_le_blocks

Mathlib.Combinatorics.Enumerative.Composition

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

English

If i is in blocks, then 1 ≤ i.

Русский

Если i принадлежит blocks, то i ≥ 1.

LaTeX

$$$\\text{If } i \\in \\mathrm{blocks},\\; 1 \\le i$$$

Lean4

theorem one_le_blocks {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i :=
  c.blocks_pos h

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

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

Разделы

Аффилиация

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