Documentation

Mathlib.Order.UpperLower.CompleteLattice

The complete lattice structure on UpperSet/LowerSet #

This file defines a completely distributive lattice structure on UpperSet and LowerSet, pulled back across the canonical injection (UpperSet.carrier, LowerSet.carrier) into Set α.

Notes #

Upper sets are ordered by reverse inclusion. This convention is motivated by the fact that this makes them order-isomorphic to lower sets and antichains, and matches the convention on Filter.

instance UpperSet.instSetLike {α : Type u_1} [LE α] :
Equations
def UpperSet.Simps.coe {α : Type u_1} [LE α] (s : UpperSet α) :
Set α

See Note [custom simps projection].

Equations
Instances For
    theorem UpperSet.ext {α : Type u_1} [LE α] {s t : UpperSet α} :
    s = ts = t
    @[simp]
    theorem UpperSet.carrier_eq_coe {α : Type u_1} [LE α] (s : UpperSet α) :
    s.carrier = s
    @[simp]
    theorem UpperSet.upper {α : Type u_1} [LE α] (s : UpperSet α) :
    @[simp]
    theorem UpperSet.coe_mk {α : Type u_1} [LE α] (s : Set α) (hs : IsUpperSet s) :
    { carrier := s, upper' := hs } = s
    @[simp]
    theorem UpperSet.mem_mk {α : Type u_1} [LE α] {s : Set α} (hs : IsUpperSet s) {a : α} :
    a { carrier := s, upper' := hs } a s
    instance LowerSet.instSetLike {α : Type u_1} [LE α] :
    Equations
    def LowerSet.Simps.coe {α : Type u_1} [LE α] (s : LowerSet α) :
    Set α

    See Note [custom simps projection].

    Equations
    Instances For
      theorem LowerSet.ext {α : Type u_1} [LE α] {s t : LowerSet α} :
      s = ts = t
      @[simp]
      theorem LowerSet.carrier_eq_coe {α : Type u_1} [LE α] (s : LowerSet α) :
      s.carrier = s
      @[simp]
      theorem LowerSet.lower {α : Type u_1} [LE α] (s : LowerSet α) :
      @[simp]
      theorem LowerSet.coe_mk {α : Type u_1} [LE α] (s : Set α) (hs : IsLowerSet s) :
      { carrier := s, lower' := hs } = s
      @[simp]
      theorem LowerSet.mem_mk {α : Type u_1} [LE α] {s : Set α} (hs : IsLowerSet s) {a : α} :
      a { carrier := s, lower' := hs } a s
      instance UpperSet.instMax {α : Type u_1} [LE α] :
      Equations
      instance UpperSet.instMin {α : Type u_1} [LE α] :
      Equations
      instance UpperSet.instTop {α : Type u_1} [LE α] :
      Equations
      instance UpperSet.instBot {α : Type u_1} [LE α] :
      Equations
      instance UpperSet.instSupSet {α : Type u_1} [LE α] :
      Equations
      instance UpperSet.instInfSet {α : Type u_1} [LE α] :
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      instance UpperSet.instInhabited {α : Type u_1} [LE α] :
      Equations
      @[simp]
      theorem UpperSet.coe_subset_coe {α : Type u_1} [LE α] {s t : UpperSet α} :
      s t t s
      @[simp]
      theorem UpperSet.coe_ssubset_coe {α : Type u_1} [LE α] {s t : UpperSet α} :
      s t t < s
      @[simp]
      theorem UpperSet.coe_top {α : Type u_1} [LE α] :
      =
      @[simp]
      theorem UpperSet.coe_bot {α : Type u_1} [LE α] :
      @[simp]
      theorem UpperSet.coe_eq_univ {α : Type u_1} [LE α] {s : UpperSet α} :
      s = Set.univ s =
      @[simp]
      theorem UpperSet.coe_eq_empty {α : Type u_1} [LE α] {s : UpperSet α} :
      s = s =
      @[simp]
      theorem UpperSet.coe_nonempty {α : Type u_1} [LE α] {s : UpperSet α} :
      (↑s).Nonempty s
      @[simp]
      theorem UpperSet.coe_sup {α : Type u_1} [LE α] (s t : UpperSet α) :
      ↑(s t) = s t
      @[simp]
      theorem UpperSet.coe_inf {α : Type u_1} [LE α] (s t : UpperSet α) :
      ↑(s t) = s t
      @[simp]
      theorem UpperSet.coe_sSup {α : Type u_1} [LE α] (S : Set (UpperSet α)) :
      (sSup S) = sS, s
      @[simp]
      theorem UpperSet.coe_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) :
      (sInf S) = sS, s
      @[simp]
      theorem UpperSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιUpperSet α) :
      (⨆ (i : ι), f i) = ⋂ (i : ι), (f i)
      @[simp]
      theorem UpperSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιUpperSet α) :
      (⨅ (i : ι), f i) = ⋃ (i : ι), (f i)
      theorem UpperSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iUpperSet α) :
      (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), (f i j)
      theorem UpperSet.coe_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iUpperSet α) :
      (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), (f i j)
      @[simp]
      theorem UpperSet.not_mem_top {α : Type u_1} [LE α] {a : α} :
      a
      @[simp]
      theorem UpperSet.mem_bot {α : Type u_1} [LE α] {a : α} :
      @[simp]
      theorem UpperSet.mem_sup_iff {α : Type u_1} [LE α] {s t : UpperSet α} {a : α} :
      a s t a s a t
      @[simp]
      theorem UpperSet.mem_inf_iff {α : Type u_1} [LE α] {s t : UpperSet α} {a : α} :
      a s t a s a t
      @[simp]
      theorem UpperSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} :
      a sSup S sS, a s
      @[simp]
      theorem UpperSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} :
      a sInf S sS, a s
      @[simp]
      theorem UpperSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ιUpperSet α} :
      a ⨆ (i : ι), f i ∀ (i : ι), a f i
      @[simp]
      theorem UpperSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ιUpperSet α} :
      a ⨅ (i : ι), f i ∃ (i : ι), a f i
      theorem UpperSet.mem_iSup₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {a : α} {f : (i : ι) → κ iUpperSet α} :
      a ⨆ (i : ι), ⨆ (j : κ i), f i j ∀ (i : ι) (j : κ i), a f i j
      theorem UpperSet.mem_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {a : α} {f : (i : ι) → κ iUpperSet α} :
      a ⨅ (i : ι), ⨅ (j : κ i), f i j ∃ (i : ι) (j : κ i), a f i j
      @[simp]
      theorem UpperSet.codisjoint_coe {α : Type u_1} [LE α] {s t : UpperSet α} :
      Codisjoint s t Disjoint s t
      instance LowerSet.instMax {α : Type u_1} [LE α] :
      Equations
      instance LowerSet.instMin {α : Type u_1} [LE α] :
      Equations
      instance LowerSet.instTop {α : Type u_1} [LE α] :
      Equations
      instance LowerSet.instBot {α : Type u_1} [LE α] :
      Equations
      instance LowerSet.instSupSet {α : Type u_1} [LE α] :
      Equations
      instance LowerSet.instInfSet {α : Type u_1} [LE α] :
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      instance LowerSet.instInhabited {α : Type u_1} [LE α] :
      Equations
      theorem LowerSet.coe_subset_coe {α : Type u_1} [LE α] {s t : LowerSet α} :
      s t s t
      theorem LowerSet.coe_ssubset_coe {α : Type u_1} [LE α] {s t : LowerSet α} :
      s t s < t
      @[simp]
      theorem LowerSet.coe_top {α : Type u_1} [LE α] :
      @[simp]
      theorem LowerSet.coe_bot {α : Type u_1} [LE α] :
      =
      @[simp]
      theorem LowerSet.coe_eq_univ {α : Type u_1} [LE α] {s : LowerSet α} :
      s = Set.univ s =
      @[simp]
      theorem LowerSet.coe_eq_empty {α : Type u_1} [LE α] {s : LowerSet α} :
      s = s =
      @[simp]
      theorem LowerSet.coe_nonempty {α : Type u_1} [LE α] {s : LowerSet α} :
      (↑s).Nonempty s
      @[simp]
      theorem LowerSet.coe_sup {α : Type u_1} [LE α] (s t : LowerSet α) :
      ↑(s t) = s t
      @[simp]
      theorem LowerSet.coe_inf {α : Type u_1} [LE α] (s t : LowerSet α) :
      ↑(s t) = s t
      @[simp]
      theorem LowerSet.coe_sSup {α : Type u_1} [LE α] (S : Set (LowerSet α)) :
      (sSup S) = sS, s
      @[simp]
      theorem LowerSet.coe_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) :
      (sInf S) = sS, s
      @[simp]
      theorem LowerSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιLowerSet α) :
      (⨆ (i : ι), f i) = ⋃ (i : ι), (f i)
      @[simp]
      theorem LowerSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιLowerSet α) :
      (⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
      theorem LowerSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iLowerSet α) :
      (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), (f i j)
      theorem LowerSet.coe_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iLowerSet α) :
      (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), (f i j)
      @[simp]
      theorem LowerSet.mem_top {α : Type u_1} [LE α] {a : α} :
      @[simp]
      theorem LowerSet.not_mem_bot {α : Type u_1} [LE α] {a : α} :
      a
      @[simp]
      theorem LowerSet.mem_sup_iff {α : Type u_1} [LE α] {s t : LowerSet α} {a : α} :
      a s t a s a t
      @[simp]
      theorem LowerSet.mem_inf_iff {α : Type u_1} [LE α] {s t : LowerSet α} {a : α} :
      a s t a s a t
      @[simp]
      theorem LowerSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} :
      a sSup S sS, a s
      @[simp]
      theorem LowerSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} :
      a sInf S sS, a s
      @[simp]
      theorem LowerSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ιLowerSet α} :
      a ⨆ (i : ι), f i ∃ (i : ι), a f i
      @[simp]
      theorem LowerSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ιLowerSet α} :
      a ⨅ (i : ι), f i ∀ (i : ι), a f i
      theorem LowerSet.mem_iSup₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {a : α} {f : (i : ι) → κ iLowerSet α} :
      a ⨆ (i : ι), ⨆ (j : κ i), f i j ∃ (i : ι) (j : κ i), a f i j
      theorem LowerSet.mem_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {a : α} {f : (i : ι) → κ iLowerSet α} :
      a ⨅ (i : ι), ⨅ (j : κ i), f i j ∀ (i : ι) (j : κ i), a f i j
      @[simp]
      theorem LowerSet.disjoint_coe {α : Type u_1} [LE α] {s t : LowerSet α} :
      Disjoint s t Disjoint s t

      Complement #

      def UpperSet.compl {α : Type u_1} [LE α] (s : UpperSet α) :

      The complement of a lower set as an upper set.

      Equations
      • s.compl = { carrier := (↑s), lower' := }
      Instances For
        def LowerSet.compl {α : Type u_1} [LE α] (s : LowerSet α) :

        The complement of a lower set as an upper set.

        Equations
        • s.compl = { carrier := (↑s), upper' := }
        Instances For
          @[simp]
          theorem UpperSet.coe_compl {α : Type u_1} [LE α] (s : UpperSet α) :
          s.compl = (↑s)
          @[simp]
          theorem UpperSet.mem_compl_iff {α : Type u_1} [LE α] {s : UpperSet α} {a : α} :
          a s.compl as
          @[simp]
          theorem UpperSet.compl_compl {α : Type u_1} [LE α] (s : UpperSet α) :
          @[simp]
          theorem UpperSet.compl_le_compl {α : Type u_1} [LE α] {s t : UpperSet α} :
          @[simp]
          theorem UpperSet.compl_sup {α : Type u_1} [LE α] (s t : UpperSet α) :
          (s t).compl = s.compl t.compl
          @[simp]
          theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s t : UpperSet α) :
          (s t).compl = s.compl t.compl
          @[simp]
          theorem UpperSet.compl_top {α : Type u_1} [LE α] :
          @[simp]
          theorem UpperSet.compl_bot {α : Type u_1} [LE α] :
          @[simp]
          theorem UpperSet.compl_sSup {α : Type u_1} [LE α] (S : Set (UpperSet α)) :
          (sSup S).compl = sS, s.compl
          @[simp]
          theorem UpperSet.compl_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) :
          (sInf S).compl = sS, s.compl
          @[simp]
          theorem UpperSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιUpperSet α) :
          (⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
          @[simp]
          theorem UpperSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιUpperSet α) :
          (⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
          theorem UpperSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iUpperSet α) :
          (⨆ (i : ι), ⨆ (j : κ i), f i j).compl = ⨆ (i : ι), ⨆ (j : κ i), (f i j).compl
          theorem UpperSet.compl_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iUpperSet α) :
          (⨅ (i : ι), ⨅ (j : κ i), f i j).compl = ⨅ (i : ι), ⨅ (j : κ i), (f i j).compl
          @[simp]
          theorem LowerSet.coe_compl {α : Type u_1} [LE α] (s : LowerSet α) :
          s.compl = (↑s)
          @[simp]
          theorem LowerSet.mem_compl_iff {α : Type u_1} [LE α] {s : LowerSet α} {a : α} :
          a s.compl as
          @[simp]
          theorem LowerSet.compl_compl {α : Type u_1} [LE α] (s : LowerSet α) :
          @[simp]
          theorem LowerSet.compl_le_compl {α : Type u_1} [LE α] {s t : LowerSet α} :
          theorem LowerSet.compl_sup {α : Type u_1} [LE α] (s t : LowerSet α) :
          (s t).compl = s.compl t.compl
          theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s t : LowerSet α) :
          (s t).compl = s.compl t.compl
          theorem LowerSet.compl_top {α : Type u_1} [LE α] :
          theorem LowerSet.compl_bot {α : Type u_1} [LE α] :
          theorem LowerSet.compl_sSup {α : Type u_1} [LE α] (S : Set (LowerSet α)) :
          (sSup S).compl = sS, s.compl
          theorem LowerSet.compl_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) :
          (sInf S).compl = sS, s.compl
          theorem LowerSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιLowerSet α) :
          (⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
          theorem LowerSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ιLowerSet α) :
          (⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
          @[simp]
          theorem LowerSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iLowerSet α) :
          (⨆ (i : ι), ⨆ (j : κ i), f i j).compl = ⨆ (i : ι), ⨆ (j : κ i), (f i j).compl
          @[simp]
          theorem LowerSet.compl_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ iLowerSet α) :
          (⨅ (i : ι), ⨅ (j : κ i), f i j).compl = ⨅ (i : ι), ⨅ (j : κ i), (f i j).compl
          def upperSetIsoLowerSet {α : Type u_1} [LE α] :

          Upper sets are order-isomorphic to lower sets under complementation.

          Equations
          Instances For
            @[simp]
            theorem upperSetIsoLowerSet_apply {α : Type u_1} [LE α] (s : UpperSet α) :
            instance UpperSet.isTotal_le {α : Type u_1} [LinearOrder α] :
            IsTotal (UpperSet α) fun (x1 x2 : UpperSet α) => x1 x2
            instance LowerSet.isTotal_le {α : Type u_1} [LinearOrder α] :
            IsTotal (LowerSet α) fun (x1 x2 : LowerSet α) => x1 x2
            def UpperSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :

            An order isomorphism of Preorders induces an order isomorphism of their upper sets.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem UpperSet.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :
              (map f).symm = map f.symm
              @[simp]
              theorem UpperSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α ≃o β} {s : UpperSet α} {b : β} :
              b (map f) s f.symm b s
              @[simp]
              @[simp]
              theorem UpperSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : UpperSet α} (g : β ≃o γ) (f : α ≃o β) :
              (map g) ((map f) s) = (map (f.trans g)) s
              @[simp]
              theorem UpperSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) :
              ((map f) s) = f '' s
              def LowerSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :

              An order isomorphism of Preorders induces an order isomorphism of their lower sets.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem LowerSet.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :
                (map f).symm = map f.symm
                @[simp]
                theorem LowerSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {f : α ≃o β} {b : β} :
                b (map f) s f.symm b s
                @[simp]
                @[simp]
                theorem LowerSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : LowerSet α} (g : β ≃o γ) (f : α ≃o β) :
                (map g) ((map f) s) = (map (f.trans g)) s
                @[simp]
                theorem LowerSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) :
                ((map f) s) = f '' s
                @[simp]
                theorem UpperSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) :
                ((map f) s).compl = (LowerSet.map f) s.compl
                @[simp]
                theorem LowerSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) :
                ((map f) s).compl = (UpperSet.map f) s.compl