Commit 2024-07-10 15:41 5b4d4576

feat(Order/Atoms): strong atomicity typeclass (#14004) A strongly atomic preorder is one in which every nontrivial interval [a,b] contains an element covering a, or equivalently an order where every closed interval is atomic. We add a new typeclass IsStronglyAtomic to capture this. We provide instances of this typeclass for SuccOrders, orders with WellFoundedLT, atomistic upper-modular lattices, complemented atomic modular lattices, and OrdConnected subtypes. We also show that such orders are atomic. We also provide the dual typeclass IsStronglyCoatomic and dual versions of all of the above.