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.

• order.pfilter P: The type of nonempty, downward directed, upward closed subsets of P. This is dual to order.ideal, so it simply wraps order.ideal Pᵒᵈ.
• order.is_pfilter P: a predicate for when a set P is a filter.

Note the relation between order/filter and order/pfilter: for any type α, filter α represents the same mathematical object as pfilter (set α).

## Tags #

pfilter, filter, ideal, dual

structure order.pfilter (P : Type u_2) [preorder P] :
Type u_2
• dual :

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) :
Prop

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

Equations
theorem order.is_pfilter.of_def {P : Type u_1} [preorder P] {F : set P} (nonempty : F.nonempty) (directed : 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.

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

A filter on P is a subset of P.

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

For the notation x ∈ F.

Equations
@[simp]
theorem order.pfilter.mem_coe {P : Type u_1} [preorder P] {x : P} (F : order.pfilter P) :
x F x F
theorem order.pfilter.is_pfilter {P : Type u_1} [preorder P] (F : order.pfilter P) :
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
@[ext]
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]
def order.pfilter.partial_order {P : Type u_1} [preorder P] :

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

Equations
@[trans]
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
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_def {P : Type u_1} [preorder P] (x : P) (I : order.ideal Pᵒᵈ) :
x {dual := I}
@[simp]
theorem order.pfilter.principal_le_iff {P : Type u_1} [preorder P] {x : P} {F : order.pfilter P} :
x F
@[simp]
theorem order.pfilter.mem_principal {P : Type u_1} [preorder P] {x y : P} :
y x
theorem order.pfilter.antitone_principal {P : Type u_1} [preorder P] :
theorem order.pfilter.principal_le_principal_iff {P : Type u_1} [preorder P] {p q : P} :
@[simp]
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]
def order.pfilter.order_bot {P : Type u_1} [preorder P] [order_top P] :

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

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

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

Equations
theorem order.pfilter.inf_mem {P : Type u_1} {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.

@[simp]
theorem order.pfilter.inf_mem_iff {P : Type u_1} {x y : P} {F : order.pfilter P} :
x y F x F y F
theorem order.pfilter.Inf_gc {P : Type u_1}  :
galois_connection (λ (x : P), (λ (F : ᵒᵈ),
def order.pfilter.Inf_gi {P : Type u_1}  :
galois_coinsertion (λ (x : P), (λ (F : ᵒᵈ),

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

Equations