mathlib3 documentation


Order filters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
Instances for order.pfilter
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 y x F y F) :

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

@[protected, instance]

A filter on P is a subset of P.

@[protected, instance]

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.mem_of_le {P : Type u_1} [preorder P] {x y : P} {F : order.pfilter P} :
x y x F y F
theorem order.pfilter.ext {P : Type u_1} [preorder P] (s t : order.pfilter P) (h : s = t) :
s = t

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 F F G x G
def order.pfilter.principal {P : Type u_1} [preorder P] (p : P) :

The smallest filter containing a given element.

theorem order.pfilter.mem_def {P : Type u_1} [preorder P] (x : P) (I : order.ideal Pᵒᵈ) :
theorem order.pfilter.principal_le_iff {P : Type u_1} [preorder P] {x : P} {F : order.pfilter P} :
theorem order.pfilter.mem_principal {P : Type u_1} [preorder P] {x y : 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] {x y : P} {F : order.pfilter P} (hx : x F) (hy : 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

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