index — Mathlib

English

For j ∈ Fin n, the index function assigns the corresponding block index in Fin c.length.

Русский

Для j ∈ Fin n функция index назначает соответствующий индекс блока в Fin c.length.

LaTeX

$$$\\text{index} : \\mathrm{Fin}(n) \\to \\mathrm{Fin}(c.length)$$$

Lean4

/-- Given `j : Fin n`, the index of the part to which it belongs. -/
noncomputable def index (j : Fin n) : Fin c.length :=
  (c.exists_inverse j).choose.1

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