English
Let P be a preorder. If F ⊆ P is nonempty, directedOn (≥) F, and upward closed (x ≤ y and x ∈ F imply y ∈ F), then F is a P-filter.
Русский
Пусть P — предсоединённое множество. Если F ⊆ P непусто, F направленно относительно ≥ и замкнуто сверху по отношению к ≤ (то есть из x ≤ y и x ∈ F следует y ∈ F), то F является P-фильтром.
LaTeX
$$$$ F \\neq \\varnothing \\land \\operatorname{DirectedOn}(\\ge)(F) \\land (\\forall x,y\\,(x \\le y \\land x \\in F \\rightarrow y \\in F)) \\Rightarrow \\operatorname{IsPFilter} F. $$$$
Lean4
theorem of_def [Preorder P] {F : Set P} (nonempty : F.Nonempty) (directed : DirectedOn (· ≥ ·) F)
(mem_of_le : ∀ {x y : P}, x ≤ y → x ∈ F → y ∈ F) : IsPFilter F :=
⟨fun _ _ _ _ => mem_of_le ‹_› ‹_›, nonempty, directed⟩
