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
Instances For
    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