toPFilter — Mathlib

English

From a subset F that satisfies the P-filter predicate, one obtains a PFilter P by taking the corresponding ideal.

Русский

Из подмножества F, удовлетворяющего предикату P-фильтра, получают P-фильтр P, взяв соответствующий идеал.

LaTeX

$$$$ \\text{toPFilter}(h) = \\langle h.\\mathrm{toIdeal} \\rangle, \\quad h : \\mathrm{IsPFilter}F. $$$$

Lean4

/-- Create an element of type `Order.PFilter` from a set satisfying the predicate
`Order.IsPFilter`. -/
def toPFilter [Preorder P] {F : Set P} (h : IsPFilter F) : PFilter P :=
  ⟨h.toIdeal⟩

Похожие утверждения