blocks_pos'

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.blocks_pos'

English

For i with i < c.length, 0 < c.blocks[i].

Русский

Для i с i < c.length, 0 < c.blocks[i].

LaTeX

$$$0 < c.blocks[i] \\quad\\text{если } i < c.length$$$

Lean4

@[simp]
theorem blocks_pos' (i : ℕ) (h : i < c.length) : 0 < c.blocks[i] :=
  c.one_le_blocks' h

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

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

Разделы

Аффилиация

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