blocksFun — Mathlib

English

For a composition, the i-th block size equals the difference between consecutive partial sums: b_i = B_i - B_{i-1}, where B0 = 0 and Bl = n.

Русский

Для разложения размер i-го блока равен разности последовательных частичных сумм: b_i = B_i - B_{i-1}, где B_0 = 0 и B_l = n.

LaTeX

$$$b_i = B_i - B_{i-1}\\quad(1\\le i\\le l),\\quad B_0=0,\\quad B_l=n,$$$

Lean4

/-- Size of the `i`-th block in a `CompositionAsSet`, seen as a function on `Fin c.length`. -/
def blocksFun (i : Fin c.length) : ℕ :=
  c.boundary ⟨(i : ℕ) + 1, c.lt_length i⟩ - c.boundary ⟨i, c.lt_length' i⟩

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