Documentation

Mathlib.Order.UpperLower.LocallyFinite

Upper and lower sets in a locally finite order #

In this file we characterise the interaction of UpperSet/LowerSet and LocallyFiniteOrder.