boundary_length — Mathlib

English

Let c be a composition of n into l blocks. If B0 = 0 and Bi = B(i-1) + b_i where (b1,...,bl) are the block sizes, then Bl = n (i.e. the total sum equals n).

Русский

Пусть c—разложение числа n на l блоков. Обозначим B0 = 0 и Bi = B(i-1) + b_i, где (b1,...,bl) — размеры блоков. Тогда Bl = n (итого сумма блоков равна n).

LaTeX

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

Lean4

@[simp]
theorem boundary_length : c.boundary ⟨c.length, c.length_lt_card_boundaries⟩ = Fin.last n :=
  by
  convert Finset.orderEmbOfFin_last rfl c.card_boundaries_pos
  exact le_antisymm (Finset.le_max' _ _ c.getLast_mem) (Fin.le_last _)

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