index — Mathlib

English

For any j in Fin n, j is less than the end of the block containing j, i.e., less than sizeUpTo(index j) plus the block size.

Русский

Для любого j ∈ Fin n, j меньше конца соответствующего блока, то есть меньше sizeUpTo(index j) + blocksFun(index j).

LaTeX

$$$(j : Fin n) \\; < \\; c.sizeUpTo(c.index(j)).succ$$$

Lean4

/-- `c.index j` is the index of the block in the composition `c` containing `j`. -/
def index (j : Fin n) : Fin c.length :=
  ⟨Nat.find (c.index_exists j.2), (Nat.find_spec (c.index_exists j.2)).2⟩

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