Documentation

Mathlib.Order.PFilter

Order filters #

Main definitions #

Throughout this file, P is at least a preorder, but some sections require more structure, such as a bottom element, a top element, or a join-semilattice structure.

Note the relation between Order/Filter and Order/PFilter: for any type α, Filter α represents the same mathematical object as PFilter (Set α).

References #

Tags #

pfilter, filter, ideal, dual

structure Order.PFilter (P : Type u_1) [Preorder P] :
Type u_1

A filter on a preorder P is a subset of P that is

  • nonempty
  • downward directed
  • upward closed.
def Order.IsPFilter {P : Type u_1} [Preorder P] (F : Set P) :

A predicate for when a subset of P is a filter.

Equations
theorem Order.IsPFilter.of_def {P : Type u_1} [Preorder P] {F : Set P} (nonempty : F.Nonempty) (directed : DirectedOn (fun (x1 x2 : P) => x1 x2) F) (mem_of_le : ∀ {x y : P}, x yx Fy F) :
def Order.IsPFilter.toPFilter {P : Type u_1} [Preorder P] {F : Set P} (h : IsPFilter F) :

Create an element of type Order.PFilter from a set satisfying the predicate Order.IsPFilter.

Equations
instance Order.PFilter.instSetLike {P : Type u_1} [Preorder P] :

A filter on P is a subset of P.

Equations
theorem Order.PFilter.isPFilter {P : Type u_1} [Preorder P] (F : PFilter P) :
theorem Order.PFilter.nonempty {P : Type u_1} [Preorder P] (F : PFilter P) :
(↑F).Nonempty
theorem Order.PFilter.directed {P : Type u_1} [Preorder P] (F : PFilter P) :
DirectedOn (fun (x1 x2 : P) => x1 x2) F
theorem Order.PFilter.mem_of_le {P : Type u_1} [Preorder P] {x y : P} {F : PFilter P} :
x yx Fy F
theorem Order.PFilter.ext {P : Type u_1} [Preorder P] (s t : PFilter P) (h : s = t) :
s = t

Two filters are equal when their underlying sets are equal.

theorem Order.PFilter.ext_iff {P : Type u_1} [Preorder P] {s t : PFilter P} :
s = t s = t
theorem Order.PFilter.mem_of_mem_of_le {P : Type u_1} [Preorder P] {x : P} {F G : PFilter P} (hx : x F) (hle : F G) :
x G
def Order.PFilter.principal {P : Type u_1} [Preorder P] (p : P) :

The smallest filter containing a given element.

Equations
@[simp]
theorem Order.PFilter.mem_mk {P : Type u_1} [Preorder P] (x : P) (I : Ideal Pᵒᵈ) :
x { dual := I } OrderDual.toDual x I
@[simp]
theorem Order.PFilter.principal_le_iff {P : Type u_1} [Preorder P] {x : P} {F : PFilter P} :
@[simp]
theorem Order.PFilter.mem_principal {P : Type u_1} [Preorder P] {x y : P} :
@[simp]
theorem Order.PFilter.top_mem {P : Type u_1} [Preorder P] [OrderTop P] {F : PFilter P} :

A specific witness of pfilter.nonempty when P has a top element.

There is a bottom filter when P has a top element.

Equations

There is a top filter when P has a bottom element.

Equations
theorem Order.PFilter.inf_mem {P : Type u_1} [SemilatticeInf P] {x y : P} {F : PFilter P} (hx : x F) (hy : y F) :
xy F

A specific witness of pfilter.directed when P has meets.

@[simp]
theorem Order.PFilter.inf_mem_iff {P : Type u_1} [SemilatticeInf P] {x y : P} {F : PFilter P} :
xy F x F y F

If a poset P admits arbitrary Infs, then principal and Inf form a Galois coinsertion.

Equations