Documentation

Mathlib.Order.UpperLower.Closure

Upper and lower closures #

Upper (lower) closures generalise principal upper (lower) sets to arbitrary included sets. Indeed, they are equivalent to a union over principal upper (lower) sets, as shown in coe_upperClosure (coe_lowerClosure).

Main declarations #

def upperClosure {α : Type u_1} [Preorder α] (s : Set α) :

The greatest upper set containing a given set.

Equations
    Instances For
      def lowerClosure {α : Type u_1} [Preorder α] (s : Set α) :

      The least lower set containing a given set.

      Equations
        Instances For
          @[simp]
          theorem mem_upperClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} :
          x upperClosure s as, a x
          @[simp]
          theorem mem_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} :
          x lowerClosure s as, x a
          theorem coe_upperClosure {α : Type u_1} [Preorder α] (s : Set α) :
          (upperClosure s) = as, Set.Ici a
          theorem coe_lowerClosure {α : Type u_1} [Preorder α] (s : Set α) :
          (lowerClosure s) = as, Set.Iic a
          instance instDecidablePredMemUpperClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun (x : α) => as, a x] :
          DecidablePred fun (x : α) => x upperClosure s
          Equations
            instance instDecidablePredMemLowerClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun (x : α) => as, x a] :
            DecidablePred fun (x : α) => x lowerClosure s
            Equations
              theorem subset_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :
              s (upperClosure s)
              theorem subset_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :
              s (lowerClosure s)
              theorem upperClosure_min {α : Type u_1} [Preorder α] {s t : Set α} (h : s t) (ht : IsUpperSet t) :
              (upperClosure s) t
              theorem lowerClosure_min {α : Type u_1} [Preorder α] {s t : Set α} (h : s t) (ht : IsLowerSet t) :
              (lowerClosure s) t
              theorem IsUpperSet.upperClosure {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) :
              (upperClosure s) = s
              theorem IsLowerSet.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) :
              (lowerClosure s) = s
              @[simp]
              theorem UpperSet.upperClosure {α : Type u_1} [Preorder α] (s : UpperSet α) :
              @[simp]
              theorem LowerSet.lowerClosure {α : Type u_1} [Preorder α] (s : LowerSet α) :
              @[simp]
              theorem upperClosure_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (f : α ≃o β) :
              @[simp]
              theorem lowerClosure_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (f : α ≃o β) :
              @[simp]
              theorem UpperSet.iInf_Ici {α : Type u_1} [Preorder α] (s : Set α) :
              as, Ici a = upperClosure s
              @[simp]
              theorem LowerSet.iSup_Iic {α : Type u_1} [Preorder α] (s : Set α) :
              as, Iic a = lowerClosure s
              @[simp]
              theorem lowerClosure_le {α : Type u_1} [Preorder α] {s : Set α} {t : LowerSet α} :
              lowerClosure s t s t
              @[simp]
              theorem le_upperClosure {α : Type u_1} [Preorder α] {t : Set α} {s : UpperSet α} :
              s upperClosure t t s

              upperClosure forms a reversed Galois insertion with the coercion from upper sets to sets.

              Equations
                Instances For

                  lowerClosure forms a Galois insertion with the coercion from lower sets to sets.

                  Equations
                    Instances For
                      @[simp]
                      @[simp]
                      @[simp]
                      theorem upperClosure_singleton {α : Type u_1} [Preorder α] (a : α) :
                      @[simp]
                      theorem lowerClosure_singleton {α : Type u_1} [Preorder α] (a : α) :
                      @[simp]
                      theorem upperClosure_eq_top_iff {α : Type u_1} [Preorder α] {s : Set α} :
                      @[simp]
                      theorem lowerClosure_eq_bot_iff {α : Type u_1} [Preorder α] {s : Set α} :
                      @[simp]
                      theorem upperClosure_union {α : Type u_1} [Preorder α] (s t : Set α) :
                      @[simp]
                      theorem lowerClosure_union {α : Type u_1} [Preorder α] (s t : Set α) :
                      @[simp]
                      theorem upperClosure_iUnion {α : Type u_1} {ι : Sort u_3} [Preorder α] (f : ιSet α) :
                      upperClosure (⋃ (i : ι), f i) = ⨅ (i : ι), upperClosure (f i)
                      @[simp]
                      theorem lowerClosure_iUnion {α : Type u_1} {ι : Sort u_3} [Preorder α] (f : ιSet α) :
                      lowerClosure (⋃ (i : ι), f i) = ⨆ (i : ι), lowerClosure (f i)
                      @[simp]
                      theorem upperClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) :
                      upperClosure (⋃₀ S) = sS, upperClosure s
                      @[simp]
                      theorem lowerClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) :
                      lowerClosure (⋃₀ S) = sS, lowerClosure s
                      @[simp]
                      theorem upperBounds_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :
                      @[simp]
                      theorem lowerBounds_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :
                      @[simp]
                      theorem bddAbove_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :
                      @[simp]
                      theorem bddBelow_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :
                      theorem BddAbove.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

                      Alias of the reverse direction of bddAbove_lowerClosure.

                      theorem BddAbove.of_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

                      Alias of the forward direction of bddAbove_lowerClosure.

                      theorem BddBelow.of_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :

                      Alias of the forward direction of bddBelow_upperClosure.

                      theorem BddBelow.upperClosure {α : Type u_1} [Preorder α] {s : Set α} :

                      Alias of the reverse direction of bddBelow_upperClosure.

                      @[simp]
                      theorem IsLowerSet.disjoint_upperClosure_left {α : Type u_1} [Preorder α] {s t : Set α} (ht : IsLowerSet t) :
                      @[simp]
                      theorem IsLowerSet.disjoint_upperClosure_right {α : Type u_1} [Preorder α] {s t : Set α} (hs : IsLowerSet s) :
                      @[simp]
                      theorem IsUpperSet.disjoint_lowerClosure_left {α : Type u_1} [Preorder α] {s t : Set α} (ht : IsUpperSet t) :
                      @[simp]
                      theorem IsUpperSet.disjoint_lowerClosure_right {α : Type u_1} [Preorder α] {s t : Set α} (hs : IsUpperSet s) :
                      @[simp]
                      theorem upperClosure_eq {α : Type u_1} [Preorder α] {s : Set α} :
                      @[simp]
                      theorem lowerClosure_eq {α : Type u_1} [Preorder α] {s : Set α} :
                      theorem IsAntichain.minimal_mem_upperClosure_iff_mem {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} (hs : IsAntichain (fun (x1 x2 : α) => x1 x2) s) :
                      Minimal (fun (x : α) => x upperClosure s) x x s
                      theorem IsAntichain.maximal_mem_lowerClosure_iff_mem {α : Type u_1} [PartialOrder α] {s : Set α} {x : α} (hs : IsAntichain (fun (x1 x2 : α) => x1 x2) s) :
                      Maximal (fun (x : α) => x lowerClosure s) x x s

                      Set Difference #

                      def LowerSet.sdiff {α : Type u_1} [Preorder α] (s : LowerSet α) (t : Set α) :

                      The biggest lower subset of a lower set s disjoint from a set t.

                      Equations
                        Instances For
                          def LowerSet.erase {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) :

                          The biggest lower subset of a lower set s not containing an element a.

                          Equations
                            Instances For
                              @[simp]
                              theorem LowerSet.coe_sdiff {α : Type u_1} [Preorder α] (s : LowerSet α) (t : Set α) :
                              (s.sdiff t) = s \ (upperClosure t)
                              @[simp]
                              theorem LowerSet.coe_erase {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) :
                              (s.erase a) = s \ (UpperSet.Ici a)
                              @[simp]
                              theorem LowerSet.sdiff_singleton {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) :
                              s.sdiff {a} = s.erase a
                              theorem LowerSet.sdiff_le_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} :
                              s.sdiff t s
                              theorem LowerSet.erase_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :
                              s.erase a s
                              @[simp]
                              theorem LowerSet.sdiff_eq_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} :
                              s.sdiff t = s Disjoint (↑s) t
                              @[simp]
                              theorem LowerSet.erase_eq {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :
                              s.erase a = s as
                              @[simp]
                              theorem LowerSet.sdiff_lt_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} :
                              s.sdiff t < s ¬Disjoint (↑s) t
                              @[simp]
                              theorem LowerSet.erase_lt {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :
                              s.erase a < s a s
                              @[simp]
                              theorem LowerSet.sdiff_idem {α : Type u_1} [Preorder α] (s : LowerSet α) (t : Set α) :
                              (s.sdiff t).sdiff t = s.sdiff t
                              @[simp]
                              theorem LowerSet.erase_idem {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) :
                              (s.erase a).erase a = s.erase a
                              theorem LowerSet.sdiff_sup_lowerClosure {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} (hts : t s) (hst : bs, ct, c bb t) :
                              s.sdiff tlowerClosure t = s
                              theorem LowerSet.lowerClosure_sup_sdiff {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} (hts : t s) (hst : bs, ct, c bb t) :
                              lowerClosure ts.sdiff t = s
                              theorem LowerSet.erase_sup_Iic {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a s) (has : bs, a bb = a) :
                              s.erase aIic a = s
                              theorem LowerSet.Iic_sup_erase {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a s) (has : bs, a bb = a) :
                              Iic as.erase a = s
                              def UpperSet.sdiff {α : Type u_1} [Preorder α] (s : UpperSet α) (t : Set α) :

                              The biggest upper subset of a upper set s disjoint from a set t.

                              Equations
                                Instances For
                                  def UpperSet.erase {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) :

                                  The biggest upper subset of a upper set s not containing an element a.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem UpperSet.coe_sdiff {α : Type u_1} [Preorder α] (s : UpperSet α) (t : Set α) :
                                      (s.sdiff t) = s \ (lowerClosure t)
                                      @[simp]
                                      theorem UpperSet.coe_erase {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) :
                                      (s.erase a) = s \ (LowerSet.Iic a)
                                      @[simp]
                                      theorem UpperSet.sdiff_singleton {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) :
                                      s.sdiff {a} = s.erase a
                                      theorem UpperSet.le_sdiff_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} :
                                      s s.sdiff t
                                      theorem UpperSet.le_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :
                                      s s.erase a
                                      @[simp]
                                      theorem UpperSet.sdiff_eq_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} :
                                      s.sdiff t = s Disjoint (↑s) t
                                      @[simp]
                                      theorem UpperSet.erase_eq {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :
                                      s.erase a = s as
                                      @[simp]
                                      theorem UpperSet.lt_sdiff_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} :
                                      s < s.sdiff t ¬Disjoint (↑s) t
                                      @[simp]
                                      theorem UpperSet.lt_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :
                                      s < s.erase a a s
                                      @[simp]
                                      theorem UpperSet.sdiff_idem {α : Type u_1} [Preorder α] (s : UpperSet α) (t : Set α) :
                                      (s.sdiff t).sdiff t = s.sdiff t
                                      @[simp]
                                      theorem UpperSet.erase_idem {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) :
                                      (s.erase a).erase a = s.erase a
                                      theorem UpperSet.sdiff_inf_upperClosure {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} (hts : t s) (hst : bs, ct, b cb t) :
                                      s.sdiff tupperClosure t = s
                                      theorem UpperSet.upperClosure_inf_sdiff {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} (hts : t s) (hst : bs, ct, b cb t) :
                                      upperClosure ts.sdiff t = s
                                      theorem UpperSet.erase_inf_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a s) (has : bs, b ab = a) :
                                      s.erase aIci a = s
                                      theorem UpperSet.Ici_inf_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a s) (has : bs, b ab = a) :
                                      Ici as.erase a = s