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
        theorem UpperSet.ext_iff {α : Type u_1} [LE α] {s t : UpperSet α} :
        s = t s = 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
              theorem LowerSet.ext_iff {α : Type u_1} [LE α] {s t : LowerSet α} :
              s = t s = 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
                            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 α) :
                              (st) = s t
                              @[simp]
                              theorem UpperSet.coe_inf {α : Type u_1} [LE α] (s t : UpperSet α) :
                              (st) = 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.notMem_top {α : Type u_1} [LE α] {a : α} :
                              a
                              @[deprecated UpperSet.notMem_top (since := "2025-05-23")]
                              theorem UpperSet.not_mem_top {α : Type u_1} [LE α] {a : α} :
                              a

                              Alias of UpperSet.notMem_top.

                              @[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 st a s a t
                              @[simp]
                              theorem UpperSet.mem_inf_iff {α : Type u_1} [LE α] {s t : UpperSet α} {a : α} :
                              a st 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
                                            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 α) :
                                              (st) = s t
                                              @[simp]
                                              theorem LowerSet.coe_inf {α : Type u_1} [LE α] (s t : LowerSet α) :
                                              (st) = 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.notMem_bot {α : Type u_1} [LE α] {a : α} :
                                              a
                                              @[deprecated LowerSet.notMem_bot (since := "2025-05-23")]
                                              theorem LowerSet.not_mem_bot {α : Type u_1} [LE α] {a : α} :
                                              a

                                              Alias of LowerSet.notMem_bot.

                                              @[simp]
                                              theorem LowerSet.mem_sup_iff {α : Type u_1} [LE α] {s t : LowerSet α} {a : α} :
                                              a st a s a t
                                              @[simp]
                                              theorem LowerSet.mem_inf_iff {α : Type u_1} [LE α] {s t : LowerSet α} {a : α} :
                                              a st 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
                                                Instances For
                                                  def LowerSet.compl {α : Type u_1} [LE α] (s : LowerSet α) :

                                                  The complement of a lower set as an upper set.

                                                  Equations
                                                    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 α) :
                                                      (st).compl = s.complt.compl
                                                      @[simp]
                                                      theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s t : UpperSet α) :
                                                      (st).compl = s.complt.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 α) :
                                                      (st).compl = s.complt.compl
                                                      theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s t : LowerSet α) :
                                                      (st).compl = s.complt.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
                                                          noncomputable instance UpperSet.instLinearOrder {α : Type u_1} [LinearOrder α] :
                                                          Equations
                                                            noncomputable instance LowerSet.instLinearOrder {α : Type u_1} [LinearOrder α] :
                                                            Equations
                                                              Equations
                                                                Equations
                                                                  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
                                                                    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
                                                                        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