Documentation

Mathlib.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

structure Order.PFilter (P : Type u_1) [Preorder P] :
Type u_1

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

  • nonempty
  • downward directed
  • upward closed.
Instances For
    def Order.IsPFilter {P : Type u_1} [Preorder P] (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} [Preorder P] {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) :

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

      Equations
      Instances For
        Equations
        • Order.PFilter.instInhabited = { default := { dual := default } }

        A filter on P is a subset of P.

        Equations
        • Order.PFilter.instSetLike = { coe := fun (F : Order.PFilter P) => OrderDual.toDual ⁻¹' F.dual.carrier, coe_injective' := }
        theorem Order.PFilter.nonempty {P : Type u_1} [Preorder P] (F : Order.PFilter P) :
        (F).Nonempty
        theorem Order.PFilter.directed {P : Type u_1} [Preorder P] (F : Order.PFilter P) :
        DirectedOn (fun (x x_1 : P) => x x_1) F
        theorem Order.PFilter.mem_of_le {P : Type u_1} [Preorder P] {x : P} {y : P} {F : Order.PFilter P} :
        x yx Fy F
        theorem Order.PFilter.ext {P : Type u_1} [Preorder P] (s : Order.PFilter P) (t : Order.PFilter P) (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} [Preorder P] {x : P} {F : Order.PFilter P} {G : Order.PFilter P} (hx : x F) (hle : F G) :
        x G
        def Order.PFilter.principal {P : Type u_1} [Preorder P] (p : P) :

        The smallest filter containing a given element.

        Equations
        Instances For
          @[simp]
          theorem Order.PFilter.mem_mk {P : Type u_1} [Preorder P] (x : P) (I : Order.Ideal Pᵒᵈ) :
          x { dual := I } OrderDual.toDual x I
          @[simp]
          @[simp]
          theorem Order.PFilter.mem_principal {P : Type u_1} [Preorder P] {x : P} {y : P} :
          theorem Order.PFilter.antitone_principal {P : Type u_1} [Preorder P] :
          Antitone Order.PFilter.principal
          @[simp]
          theorem Order.PFilter.top_mem {P : Type u_1} [Preorder P] [OrderTop P] {F : Order.PFilter P} :

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

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

          Equations

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

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