English
The inverse embedding maps j to a finite index in the appropriate part, i.e., invEmbedding(j) ∈ Fin (c.partSize (c.index j)).
Русский
Обратное вложение переводит j в конечный индекс внутри соответствующей части: invEmbedding(j) ∈ Fin (c.partSize (c.index j)).
LaTeX
$$$\\mathrm{invEmbedding}(j) : \\mathrm{Fin}(c.partSize (c.index j))$$$
Lean4
/-- The inverse of `c.emb` for `c : OrderedFinpartition`. It maps `j : Fin n` to the point in
`Fin (c.partSize (c.index j))` which is mapped back to `j` by `c.emb (c.index j)`. -/
noncomputable def invEmbedding (j : Fin n) : Fin (c.partSize (c.index j)) :=
(c.exists_inverse j).choose.2