Documentation

Mathlib.Order.Interval.Finset.Box

Decomposing a locally finite ordered ring into boxes #

This file proves that any locally finite ordered ring can be decomposed into "boxes", namely differences of consecutive intervals.

Implementation notes #

We don't need the full ring structure, only that there is an order embedding ℤ →

General locally finite ordered ring #

source
def Finset.box {α : Type u_1} [Ring α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] :
ℕ → Finset α

Hollow box centered at 0 : α going from -n to n.

Equations
source
@[simp]
theorem Finset.box_zero {α : Type u_1} [Ring α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] :
box 0 = {0}
source
theorem Finset.box_succ_eq_sdiff {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) :
box (n + 1) = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n
source
theorem Finset.disjoint_box_succ_prod {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) :
Disjoint (box (n + 1)) (Icc (-↑n) ↑n)
source
@[simp]
theorem Finset.box_succ_union_prod {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) :
box (n + 1) ∪ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ
source
theorem Finset.box_succ_disjUnion {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) :
(box (n + 1)).disjUnion (Icc (-↑n) ↑n) ⋯ = Icc (-↑n.succ) ↑n.succ
source
@[simp]
theorem Finset.zero_mem_box {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [LocallyFiniteOrder α] {n : ℕ} [DecidableEq α] :
0 ∈ box n ↔ n = 0
source
theorem Finset.eq_zero_iff_eq_zero_of_mem_box {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] [LocallyFiniteOrder α] {n : ℕ} [DecidableEq α] {x : α} (hx : x ∈ box n) :
x = 0 ↔ n = 0

Product of locally finite ordered rings #

source
@[simp]
theorem Prod.card_box_succ {α : Type u_1} {β : Type u_2} [Ring α] [PartialOrder α] [IsOrderedRing α] [Ring β] [PartialOrder β] [IsOrderedRing β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableEq α] [DecidableEq β] [DecidableLE (α × β)] (n : ℕ) :
(Finset.box (n + 1)).card = (Finset.Icc (-↑n.succ) ↑n.succ).card * (Finset.Icc (-↑n.succ) ↑n.succ).card - (Finset.Icc (-↑n) ↑n).card * (Finset.Icc (-↑n) ↑n).card

ℤ × ℤ #

source
theorem Int.card_box {n : ℕ} :
n ≠ 0 → (Finset.box n).card = 8 * n
source
@[simp]
theorem Int.mem_box {x : ℤ × ℤ} {n : ℕ} :
x ∈ Finset.box n ↔ max x.1.natAbs x.2.natAbs = n
source
theorem Int.existsUnique_mem_box (x : ℤ × ℤ) :
∃! n : ℕ, x ∈ Finset.box n