box — Mathlib

English

The box is the set of all n-tuples with entries in {0,1,...,d-1}. More formally, the Finset box(n,d) represents the collection of all functions from Fin n to Fin d, i.e., {0,...,d-1}^n.

Русский

Коробка box(n,d) описывает множество всех n-кубов с координатами в {0,1,...,d-1}, то есть множество функций из Fin n в Fin d, т.е. {0,...,d-1}^n.

LaTeX

$$$$ \mathrm{box}(n,d) = \mathrm{Finset}\big(\mathrm{Fin}(n) \to \mathrm{Fin}(d)\big). $$$$

Lean4

/-- The box `{0, ..., d - 1}^n` as a `Finset`. -/
def box (n d : ℕ) : Finset (Fin n → ℕ) :=
  Fintype.piFinset fun _ => range d

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