sizeUpTo_strict_mono

Mathlib.Combinatorics.Enumerative.Composition

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

English

For any composition c, sizeUpTo at length is equal to n and increases by each block.

Русский

Для любой композиции c, sizeUpTo(length) = n и возрастает при каждом добавлении блока.

LaTeX

$$$\\forall i < c.length, c.sizeUpTo(i+1) = c.sizeUpTo(i) + B_i$$$

Lean4

theorem sizeUpTo_strict_mono {i : ℕ} (h : i < c.length) : c.sizeUpTo i < c.sizeUpTo (i + 1) :=
  by
  rw [c.sizeUpTo_succ h]
  simp

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

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

Разделы

Аффилиация

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