mathlib3 documentation

order.pfilter

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

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.
Instances for order.pfilter
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.inhabited {P : Type u_1} [preorder P] [inhabited P] :
inhabited (order.pfilter P)
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
@[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.

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

The smallest filter containing a given element.

Equations
source
@[simp]
theorem order.pfilter.mem_def {P : Type u_1} [preorder P] (x : P) (I : order.ideal Pᵒᵈ) :
x ∈ {dual := I} ↔ ⇑order_dual.to_dual x ∈ I
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.mem_principal {P : Type u_1} [preorder P] {x y : P} :
x ∈ order.pfilter.principal y ↔ y ≤ x
source
theorem order.pfilter.antitone_principal {P : Type u_1} [preorder P] :
antitone order.pfilter.principal
source
theorem order.pfilter.principal_le_principal_iff {P : Type u_1} [preorder P] {p q : P} :
order.pfilter.principal q ≤ order.pfilter.principal p ↔ p ≤ q
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] {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.

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
source
theorem order.pfilter.Inf_gc {P : Type u_1} [complete_semilattice_Inf P] :
galois_connection (λ (x : P), ⇑order_dual.to_dual (order.pfilter.principal x)) (λ (F : (order.pfilter P)ᵒᵈ), has_Inf.Inf ↑(⇑order_dual.of_dual F))
source
def order.pfilter.Inf_gi {P : Type u_1} [complete_semilattice_Inf P] :
galois_coinsertion (λ (x : P), ⇑order_dual.to_dual (order.pfilter.principal x)) (λ (F : (order.pfilter P)ᵒᵈ), has_Inf.Inf ↑(⇑order_dual.of_dual F))

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

Equations