mem_box — Mathlib

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?

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