English
Let c be a composition of n. For every j in Fin n, the position of j inside the block containing j is j minus the total size of all preceding blocks. Equivalently, the inverse-embedding satisfies that its value equals the offset of j within its block: the element c.invEmbedding j has value j minus sizeUpTo(index j).
Русский
Пусть c — композиция числа n. Для каждого j из Fin n положение j внутри блока, содержащего j, равно j минус общая длина всех предыдущих блоков. Иными словами, значение c.invEmbedding j равно смещению j внутри своего блока: j минус суммарного размера блоков до блока, содержащего j.
LaTeX
$$$ (c.invEmbedding j).val = j.val - c.sizeUpTo (c.index j).val $$$
Lean4
/-- Mapping an element `j` of `Fin n` to the element in the block containing it, identified with
`Fin (c.blocksFun (c.index j))` through the canonical increasing bijection. -/
def invEmbedding (j : Fin n) : Fin (c.blocksFun (c.index j)) :=
⟨j - c.sizeUpTo (c.index j), by
rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']
· exact lt_sizeUpTo_index_succ _ _
· exact sizeUpTo_index_le _ _⟩
