invEmbedding — Mathlib

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

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