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