English
Let P be a preorder. A subset F ⊆ P is called a P-filter if, viewed in the opposite order, it forms an ideal. Equivalently, F is nonempty, upward closed, and directed with respect to the usual order when considered in the dual order.
Русский
Пусть P — частично упорядченное множество. Подмножество F ⊆ P называют P-фильтром, если, рассматривая F во внутреннем порядке противоположному, оно является идеалом. Эквивалентно: F не пусто, замкнуто сверху и связано направленно относительно обычного порядка в двойственном порядке.
LaTeX
$$$$ \\operatorname{IsPFilter}(F) \\iff \\operatorname{IsIdeal}(\\mathrm{OrderDual.ofDual}^{-1}F). $$$$
Lean4
/-- A predicate for when a subset of `P` is a filter. -/
def IsPFilter [Preorder P] (F : Set P) : Prop :=
IsIdeal (OrderDual.ofDual ⁻¹' F)
