English
HolorIndex ds is the type of index tuples for a holor of dimensions ds, i.e., a list is with the correct length and each entry is less than the corresponding dimension.
Русский
HolorIndex ds — множество индексов для холора размерности ds, то есть список с нужной длиной, каждый элемент меньше соответствующей размерности.
LaTeX
$$HolorIndex\; ds = { is : List\Nat // Forall₂ (<) is ds }$$
Lean4
/-- `HolorIndex ds` is the type of valid index tuples used to identify an entry of a holor
of dimensions `ds`. -/
def HolorIndex (ds : List ℕ) : Type :=
{ is : List ℕ // Forall₂ (· < ·) is ds }
