English
For x ∈ ℤ×ℤ and n ∈ ℕ, x ∈ box(n) iff max(|x1|,|x2|) = n.
Русский
Пусть x ∈ ℤ×ℤ и n ∈ ℕ. Тогда x ∈ box(n) тогда и только тогда, когда max(|x1|,|x2|) = n.
LaTeX
$$$x \in \mathrm{box}(n) \iff \max(|x_1|,|x_2|) = n$$$
Lean4
@[simp]
theorem mem_box : ∀ {n}, x ∈ box n ↔ max x.1.natAbs x.2.natAbs = n
| 0 => by simp [Prod.ext_iff]
| n + 1 => by
simp [box_succ_eq_sdiff, Prod.le_def]
omega
-- TODO: Can this be generalised to locally finite archimedean ordered rings?