English
The i-th boundary of a composition is the leftmost point of the i-th block; there is a virtual point at the right of the last block.
Русский
i-я граница композиции является левым краем i-го блока; справа от последнего блока добавляется виртуальная граница.
LaTeX
$$$\\text{boundary}(i) = \\text{sizeUpTo}(i)\\quad (i = 0,1,...,c.length)$$$
Lean4
/-- The `i`-th boundary of a composition, i.e., the leftmost point of the `i`-th block. We include
a virtual point at the right of the last block, to make for a nice equiv with
`CompositionAsSet n`. -/
def boundary : Fin (c.length + 1) ↪o Fin (n + 1) :=
(OrderEmbedding.ofStrictMono fun i => ⟨c.sizeUpTo i, Nat.lt_succ_of_le (c.sizeUpTo_le i)⟩) <|
Fin.strictMono_iff_lt_succ.2 fun ⟨_, hi⟩ => c.sizeUpTo_strict_mono hi
