one_le_blocks'

Mathlib.Combinatorics.Enumerative.Composition

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

English

For i with i < c.length, 1 ≤ c.blocks[i].

Русский

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

LaTeX

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

Lean4

@[simp]
theorem one_le_blocks' {i : ℕ} (h : i < c.length) : 1 ≤ c.blocks[i] :=
  c.one_le_blocks (get_mem (blocks c) _)

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

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

Разделы

Аффилиация

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