English
The box function on a locally finite ordered ring is defined by taking hollow shells between -n and n, i.e. box(n) is the finite set consisting of elements in the interval [-n, n] on the ring, arranged as a hollow region.
Русский
Функция box на локально конечном упорядоченном кольце задаётся как пустотный «ящик» между -n и n; box(n) — конечное множество элементов из интервала [-n, n], образующее полость.
LaTeX
$$$\mathrm{box}: \mathbb{N} \to \mathrm{Finset}\;\alpha\quad\text{with}\quad \mathrm{box}(n) = \mathrm{disjointed}\big(n \mapsto \mathrm{Icc}(-n,n)\big)$$$
Lean4
/-- Hollow box centered at `0 : α` going from `-n` to `n`. -/
def box : ℕ → Finset α :=
disjointed fun n ↦ Icc (-n : α) n
