mathlib documentation


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_2) [preorder P] :
Type u_2

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

  • nonempty
  • downward directed
  • upward closed.
def order.is_pfilter {P : Type u_1} [preorder P] (F : set P) :

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

theorem order.is_pfilter.of_def {P : Type u_1} [preorder P] {F : set P} (nonempty : F.nonempty) (directed : directed_on ge F) (mem_of_le : ∀ {x y : P}, x yx Fy F) :
def order.is_pfilter.to_pfilter {P : Type u_1} [preorder P] {F : set P} (h : order.is_pfilter F) :

Create an element of type order.pfilter from a set satisfying the predicate order.is_pfilter.

@[protected, instance]
def order.pfilter.set.has_coe {P : Type u_1} [preorder P] :

A filter on P is a subset of P.

@[protected, instance]
def order.pfilter.has_mem {P : Type u_1} [preorder P] :

For the notation x ∈ F.

theorem order.pfilter.mem_coe {P : Type u_1} [preorder P] {x : P} (F : order.pfilter P) :
x F x F
theorem order.pfilter.nonempty {P : Type u_1} [preorder P] (F : order.pfilter P) :
theorem order.pfilter.directed {P : Type u_1} [preorder P] (F : order.pfilter P) :
theorem order.pfilter.mem_of_le {P : Type u_1} [preorder P] {x y : P} {F : order.pfilter P} :
x yx Fy F
def order.pfilter.principal {P : Type u_1} [preorder P] (p : P) :

The smallest filter containing a given element.

theorem order.pfilter.ext {P : Type u_1} [preorder P] (F G : order.pfilter P) :
F = GF = G

Two filters are equal when their underlying sets are equal.

@[protected, instance]

The partial ordering by subset inclusion, inherited from set P.

theorem order.pfilter.mem_of_mem_of_le {P : Type u_1} [preorder P] {x : P} {F G : order.pfilter P} :
x FF Gx G
theorem order.pfilter.principal_le_iff {P : Type u_1} [preorder P] {x : P} {F : order.pfilter P} :
theorem order.pfilter.top_mem {P : Type u_1} [preorder P] [order_top P] {F : order.pfilter P} :

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

@[protected, instance]

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

@[protected, instance]

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

theorem order.pfilter.inf_mem {P : Type u_1} [semilattice_inf P] {F : order.pfilter P} (x : P) (H : x F) (y : P) (H_1 : y F) :
x y F

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

theorem order.pfilter.inf_mem_iff {P : Type u_1} [semilattice_inf P] {x y : P} {F : order.pfilter P} :
x y F x F y F