mathlib documentation

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

source
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.
source
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
source
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) :
order.is_pfilter F
source
def order.is_pfilter.to_pfilter {P : Type u_1} [preorder P] {F : set P} (h : order.is_pfilter F) :
order.pfilter P

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

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

A filter on P is a subset of P.

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

For the notation x ∈ F.

Equations
source
@[simp]
theorem order.pfilter.mem_coe {P : Type u_1} [preorder P] {x : P} (F : order.pfilter P) :
x ∈ ↑F ↔ x ∈ F
source
theorem order.pfilter.is_pfilter {P : Type u_1} [preorder P] (F : order.pfilter P) :
order.is_pfilter ↑F
source
theorem order.pfilter.nonempty {P : Type u_1} [preorder P] (F : order.pfilter P) :
↑F.nonempty
source
theorem order.pfilter.directed {P : Type u_1} [preorder P] (F : order.pfilter P) :
directed_on ge ↑F
source
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
source
def order.pfilter.principal {P : Type u_1} [preorder P] (p : P) :
order.pfilter P

The smallest filter containing a given element.

Equations
source
@[protected, instance]
def order.pfilter.inhabited {P : Type u_1} [preorder P] [inhabited P] :
inhabited (order.pfilter P)
Equations
source
@[ext]
theorem order.pfilter.ext {P : Type u_1} [preorder P] (F G : order.pfilter P) :
↑F = ↑G → F = G

Two filters are equal when their underlying sets are equal.

source
@[protected, instance]
def order.pfilter.partial_order {P : Type u_1} [preorder P] :
partial_order (order.pfilter P)

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

Equations
source
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
source
@[simp]
theorem order.pfilter.principal_le_iff {P : Type u_1} [preorder P] {x : P} {F : order.pfilter P} :
order.pfilter.principal x ≤ F ↔ x ∈ F
source
@[simp]
theorem order.pfilter.top_mem {P : Type u_1} [preorder P] [order_top P] {F : order.pfilter P} :
⊤ ∈ F

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

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

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

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

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

Equations
source
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.

source
@[simp]
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