Structure Order.PFilter

Modification history

2024-01-10 10:28

Mathlib/Order/PFilter.lean

chore(Order/PFilter): cosmetic improvement (#9177)

Modified Order.PFilter View on Github →

2023-02-18 15:58

Mathlib/Order/PFilter.lean

feat: port Order.Pfilter (#2351) …

Added Order.PFilter View on Github →