English
For the i-th block, there is an embedding of its local positions into all positions 0..n-1, mapping the k-th position inside the i-th block to sizeUpTo(i) + k.
Русский
Для i-го блока существует вложение локальных позиций блока в 0..n-1, отображающее k-ую позицию внутри i-го блока в sizeUpTo(i) + k.
LaTeX
$$$\\mathrm{embedding}(i)(j) = \\mathrm{sizeUpTo}(i) + j$$$
Lean4
/-- Embedding the `i`-th block of a composition (identified with `Fin (c.blocksFun i)`) into
`Fin n` at the relevant position. -/
def embedding (i : Fin c.length) : Fin (c.blocksFun i) ↪o Fin n :=
(Fin.natAddOrderEmb <| c.sizeUpTo i).trans <|
Fin.castLEOrderEmb <|
calc
c.sizeUpTo i + c.blocksFun i = c.sizeUpTo (i + 1) := (c.sizeUpTo_succ i.2).symm
_ ≤ c.sizeUpTo c.length := (monotone_sum_take _ i.2)
_ = n := c.sizeUpTo_length
