# 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.IsPFilter 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_1) [] :
Type u_1

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

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

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

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

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

Equations
• h.toPFilter = { dual := }
Instances For
instance Order.PFilter.instInhabited {P : Type u_1} [] [] :
Equations
• Order.PFilter.instInhabited = { default := { dual := default } }
instance Order.PFilter.instSetLike {P : Type u_1} [] :

A filter on P is a subset of P.

Equations
• Order.PFilter.instSetLike = { coe := fun (F : ) => OrderDual.toDual ⁻¹' F.dual.carrier, coe_injective' := }
theorem Order.PFilter.isPFilter {P : Type u_1} [] (F : ) :
theorem Order.PFilter.nonempty {P : Type u_1} [] (F : ) :
(↑F).Nonempty
theorem Order.PFilter.directed {P : Type u_1} [] (F : ) :
DirectedOn (fun (x x_1 : P) => x x_1) F
theorem Order.PFilter.mem_of_le {P : Type u_1} [] {x : P} {y : P} {F : } :
x yx Fy F
theorem Order.PFilter.ext_iff {P : Type u_1} [] {s : } {t : } :
s = t s = t
theorem Order.PFilter.ext {P : Type u_1} [] (s : ) (t : ) (h : s = t) :
s = t

Two filters are equal when their underlying sets are equal.

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

The smallest filter containing a given element.

Equations
Instances For
@[simp]
theorem Order.PFilter.mem_mk {P : Type u_1} [] (x : P) (I : ) :
x { dual := I } OrderDual.toDual x I
@[simp]
theorem Order.PFilter.principal_le_iff {P : Type u_1} [] {x : P} {F : } :
x F
@[simp]
theorem Order.PFilter.mem_principal {P : Type u_1} [] {x : P} {y : P} :
y x
theorem Order.PFilter.principal_le_principal_iff {P : Type u_1} [] {p : P} {q : P} :
theorem Order.PFilter.antitone_principal {P : Type u_1} [] :
Antitone Order.PFilter.principal
@[simp]
theorem Order.PFilter.top_mem {P : Type u_1} [] [] {F : } :

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

instance Order.PFilter.instOrderBot {P : Type u_1} [] [] :

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

Equations
• Order.PFilter.instOrderBot =
instance Order.PFilter.instOrderTopOfOrderBot {P : Type u_2} [] [] :

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

Equations
• Order.PFilter.instOrderTopOfOrderBot =
theorem Order.PFilter.inf_mem {P : Type u_1} [] {x : P} {y : P} {F : } (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 : P} {y : P} {F : } :
x y F x F y F
theorem Order.PFilter.sInf_gc {P : Type u_1} :
GaloisConnection (fun (x : P) => OrderDual.toDual ) fun (F : ᵒᵈ) => sInf (OrderDual.ofDual F)
def Order.PFilter.infGi {P : Type u_1} :
GaloisCoinsertion (fun (x : P) => OrderDual.toDual ) fun (F : ᵒᵈ) => sInf (OrderDual.ofDual F)

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

Equations
• Order.PFilter.infGi = .toGaloisCoinsertion
Instances For