Commit 2021-02-18 08:05 2a7eafa5
View on Github →feat(order/pfilter): add preorder filters, dual to preorder ideals (#5928)
Named pfilter to not conflict with the existing order/filter,
which is a much more developed theory of a special case of this.