sizeUpTo — Mathlib

English

If c is a composition of n with blocks B1,...,Bℓ, then for any i, sizeUpTo(i) equals the sum of the first i blocks, i.e. ∑_{t=1}^i B_t.

Русский

Для композиции c с блоками B1,...,Bℓ сумма размеров первых i блоков равна размерности до i: ∑_{t=1}^i B_t.

LaTeX

$$$\\mathrm{sizeUpTo}(i) = \\sum_{t=1}^{i} B_t$$$

Lean4

/-- The sum of the sizes of the blocks in a composition up to `i`. -/
def sizeUpTo (i : ℕ) : ℕ :=
  (c.blocks.take i).sum

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