Commit 2023-02-18 15:58 5efa544e

View on Github →

feat: port Order.Pfilter (#2351) I replaced Coe and Membership with SetLike since the order is not reversed (as it is for Filters).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/PFilter.lean

added theorem Order.IsPFilter.of_def

added def Order.IsPFilter.toPFilter

added def Order.IsPFilter

added theorem Order.PFilter.antitone_principal

added theorem Order.PFilter.directed

added theorem Order.PFilter.ext

added def Order.PFilter.infGi

added theorem Order.PFilter.inf_mem

added theorem Order.PFilter.inf_mem_iff

added theorem Order.PFilter.infₛ_gc

added theorem Order.PFilter.isPFilter

added theorem Order.PFilter.mem_mk

added theorem Order.PFilter.mem_of_le

added theorem Order.PFilter.mem_of_mem_of_le

added theorem Order.PFilter.mem_principal

added def Order.PFilter.principal

added theorem Order.PFilter.principal_le_iff

added theorem Order.PFilter.principal_le_principal_iff

added theorem Order.PFilter.top_mem

added structure Order.PFilter