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 #

def Finset.box {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] :
Finset α

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

Equations
Instances For
    @[simp]
    theorem Finset.box_zero {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] :
    theorem Finset.box_succ_eq_sdiff {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ) :
    Finset.box (n + 1) = Finset.Icc (-n.succ) n.succ \ Finset.Icc (-n) n
    @[simp]
    theorem Finset.box_succ_union_prod {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ) :
    Finset.box (n + 1) Finset.Icc (-n) n = Finset.Icc (-n.succ) n.succ
    theorem Finset.box_succ_disjUnion {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ) :
    (Finset.box (n + 1)).disjUnion (Finset.Icc (-n) n) = Finset.Icc (-n.succ) n.succ
    @[simp]
    theorem Finset.zero_mem_box {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] {n : } [DecidableEq α] :
    theorem Finset.eq_zero_iff_eq_zero_of_mem_box {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] {n : } [DecidableEq α] {x : α} (hx : x Finset.box n) :
    x = 0 n = 0

    Product of locally finite ordered rings #

    @[simp]
    theorem Prod.card_box_succ {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedRing β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableEq α] [DecidableEq β] [DecidableRel fun (x1 x2 : α × β) => x1 x2] (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

    ℤ × ℤ #

    theorem Int.card_box {n : } :
    n 0(Finset.box n).card = 8 * n
    @[simp]
    theorem Int.mem_box {x : × } {n : } :
    x Finset.box n max x.1.natAbs x.2.natAbs = n