mathlib

2a7eafa5 - feat(order/pfilter): add preorder filters, dual to preorder ideals (#5928)

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.