Commit 2024-02-19 17:38 8a5cead1

View on Github →

feat: Boxes in locally finite ordered rings (#10506) Define the sequence of "hollow boxes" indexed by natural numbers as the successive differences of the "boxes" Icc (-n) n.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/DFinsupp/Interval.lean

Modified Mathlib/Data/Fin/Interval.lean

Modified Mathlib/Data/Finset/Interval.lean

Renamed Mathlib/Data/Finset/LocallyFinite.lean to Mathlib/Data/Finset/LocallyFinite/Basic.lean

Created Mathlib/Data/Finset/LocallyFinite/Box.lean

added def Finset.box

added theorem Finset.box_succ_disjUnion

added theorem Finset.box_succ_eq_sdiff

added theorem Finset.box_succ_union_prod

added theorem Finset.box_zero

added theorem Finset.disjoint_box_succ_prod

added theorem Finset.zero_mem_box

added theorem Int.card_box

added theorem Int.existsUnique_mem_box

added theorem Int.mem_box

added theorem Prod.card_box_succ

Modified Mathlib/Data/Finsupp/Interval.lean

Modified Mathlib/Data/Int/Interval.lean

Modified Mathlib/Data/Multiset/Interval.lean

Modified Mathlib/Data/Multiset/LocallyFinite.lean

Modified Mathlib/Data/Nat/Interval.lean

Modified Mathlib/Data/Pi/Interval.lean

Modified Mathlib/Order/Birkhoff.lean

Modified Mathlib/Order/Disjointed.lean

deleted theorem Monotone.disjointed_eq