length_le

Mathlib.Combinatorics.Enumerative.Composition

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

English

The length of c is at most n: c.length ≤ n.

Русский

Длина c не превосходит n: c.length ≤ n.

LaTeX

$$$c.length \\le n$$$

Lean4

@[simp]
theorem length_le : c.length ≤ n := by
  conv_rhs => rw [← c.blocks_sum]
  exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi

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

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

Разделы

Аффилиация

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