Documentation

Mathlib.Order.UpperLower.Basic

Up-sets and down-sets #

This file defines upper and lower sets in an order.

Main declarations #

Notation #

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.

TODO #

Lattice structure on antichains. Order equivalence between upper/lower sets and antichains.

Unbundled upper/lower sets #

def IsUpperSet {α : Type u_1} [LE α] (s : Set α) :

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

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

    A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

    Equations
    Instances For
      theorem isUpperSet_empty {α : Type u_1} [LE α] :
      theorem isLowerSet_empty {α : Type u_1} [LE α] :
      theorem isUpperSet_univ {α : Type u_1} [LE α] :
      IsUpperSet Set.univ
      theorem isLowerSet_univ {α : Type u_1} [LE α] :
      IsLowerSet Set.univ
      theorem IsUpperSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : IsUpperSet s) :
      theorem IsLowerSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : IsLowerSet s) :
      @[simp]
      theorem isUpperSet_compl {α : Type u_1} [LE α] {s : Set α} :
      @[simp]
      theorem isLowerSet_compl {α : Type u_1} [LE α] {s : Set α} :
      theorem IsUpperSet.union {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :
      theorem IsLowerSet.union {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :
      theorem IsUpperSet.inter {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :
      theorem IsLowerSet.inter {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :
      theorem isUpperSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, IsUpperSet s) :
      theorem isLowerSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, IsLowerSet s) :
      theorem isUpperSet_iUnion {α : Type u_1} {ι : Sort u_4} [LE α] {f : ιSet α} (hf : ∀ (i : ι), IsUpperSet (f i)) :
      IsUpperSet (⋃ (i : ι), f i)
      theorem isLowerSet_iUnion {α : Type u_1} {ι : Sort u_4} [LE α] {f : ιSet α} (hf : ∀ (i : ι), IsLowerSet (f i)) :
      IsLowerSet (⋃ (i : ι), f i)
      theorem isUpperSet_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsUpperSet (f i j)) :
      IsUpperSet (⋃ (i : ι), ⋃ (j : κ i), f i j)
      theorem isLowerSet_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)) :
      IsLowerSet (⋃ (i : ι), ⋃ (j : κ i), f i j)
      theorem isUpperSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, IsUpperSet s) :
      theorem isLowerSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, IsLowerSet s) :
      theorem isUpperSet_iInter {α : Type u_1} {ι : Sort u_4} [LE α] {f : ιSet α} (hf : ∀ (i : ι), IsUpperSet (f i)) :
      IsUpperSet (⋂ (i : ι), f i)
      theorem isLowerSet_iInter {α : Type u_1} {ι : Sort u_4} [LE α] {f : ιSet α} (hf : ∀ (i : ι), IsLowerSet (f i)) :
      IsLowerSet (⋂ (i : ι), f i)
      theorem isUpperSet_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsUpperSet (f i j)) :
      IsUpperSet (⋂ (i : ι), ⋂ (j : κ i), f i j)
      theorem isLowerSet_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] {f : (i : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)) :
      IsLowerSet (⋂ (i : ι), ⋂ (j : κ i), f i j)
      @[simp]
      theorem isLowerSet_preimage_ofDual_iff {α : Type u_1} [LE α] {s : Set α} :
      IsLowerSet (OrderDual.ofDual ⁻¹' s) IsUpperSet s
      @[simp]
      theorem isUpperSet_preimage_ofDual_iff {α : Type u_1} [LE α] {s : Set α} :
      IsUpperSet (OrderDual.ofDual ⁻¹' s) IsLowerSet s
      @[simp]
      theorem isLowerSet_preimage_toDual_iff {α : Type u_1} [LE α] {s : Set αᵒᵈ} :
      IsLowerSet (OrderDual.toDual ⁻¹' s) IsUpperSet s
      @[simp]
      theorem isUpperSet_preimage_toDual_iff {α : Type u_1} [LE α] {s : Set αᵒᵈ} :
      IsUpperSet (OrderDual.toDual ⁻¹' s) IsLowerSet s
      theorem IsUpperSet.toDual {α : Type u_1} [LE α] {s : Set α} :
      IsUpperSet sIsLowerSet (OrderDual.ofDual ⁻¹' s)

      Alias of the reverse direction of isLowerSet_preimage_ofDual_iff.

      theorem IsLowerSet.toDual {α : Type u_1} [LE α] {s : Set α} :
      IsLowerSet sIsUpperSet (OrderDual.ofDual ⁻¹' s)

      Alias of the reverse direction of isUpperSet_preimage_ofDual_iff.

      theorem IsUpperSet.ofDual {α : Type u_1} [LE α] {s : Set αᵒᵈ} :
      IsUpperSet sIsLowerSet (OrderDual.toDual ⁻¹' s)

      Alias of the reverse direction of isLowerSet_preimage_toDual_iff.

      theorem IsLowerSet.ofDual {α : Type u_1} [LE α] {s : Set αᵒᵈ} :
      IsLowerSet sIsUpperSet (OrderDual.toDual ⁻¹' s)

      Alias of the reverse direction of isUpperSet_preimage_toDual_iff.

      theorem IsUpperSet.isLowerSet_preimage_coe {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) :
      IsLowerSet (Subtype.val ⁻¹' t) bs, ct, b cb t
      theorem IsLowerSet.isUpperSet_preimage_coe {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) :
      IsUpperSet (Subtype.val ⁻¹' t) bs, ct, c bb t
      theorem IsUpperSet.sdiff {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : bs, ct, b cb t) :
      theorem IsLowerSet.sdiff {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : bs, ct, c bb t) :
      theorem IsUpperSet.sdiff_of_isLowerSet {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsLowerSet t) :
      theorem IsLowerSet.sdiff_of_isUpperSet {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsUpperSet t) :
      theorem IsUpperSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : IsUpperSet s) (has : bs, b ab = a) :
      IsUpperSet (s \ {a})
      theorem IsLowerSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : IsLowerSet s) (has : bs, a bb = a) :
      IsLowerSet (s \ {a})
      theorem isUpperSet_Ici {α : Type u_1} [Preorder α] (a : α) :
      theorem isLowerSet_Iic {α : Type u_1} [Preorder α] (a : α) :
      theorem isUpperSet_Ioi {α : Type u_1} [Preorder α] (a : α) :
      theorem isLowerSet_Iio {α : Type u_1} [Preorder α] (a : α) :
      theorem isUpperSet_iff_Ici_subset {α : Type u_1} [Preorder α] {s : Set α} :
      IsUpperSet s ∀ ⦃a : α⦄, a sSet.Ici a s
      theorem isLowerSet_iff_Iic_subset {α : Type u_1} [Preorder α] {s : Set α} :
      IsLowerSet s ∀ ⦃a : α⦄, a sSet.Iic a s
      theorem IsUpperSet.Ici_subset {α : Type u_1} [Preorder α] {s : Set α} :
      IsUpperSet s∀ ⦃a : α⦄, a sSet.Ici a s

      Alias of the forward direction of isUpperSet_iff_Ici_subset.

      theorem IsLowerSet.Iic_subset {α : Type u_1} [Preorder α] {s : Set α} :
      IsLowerSet s∀ ⦃a : α⦄, a sSet.Iic a s

      Alias of the forward direction of isLowerSet_iff_Iic_subset.

      theorem IsUpperSet.Ioi_subset {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) ⦃a : α (ha : a s) :
      theorem IsLowerSet.Iio_subset {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) ⦃a : α (ha : a s) :
      theorem IsUpperSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) :
      s.OrdConnected
      theorem IsLowerSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) :
      s.OrdConnected
      theorem IsUpperSet.preimage {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsUpperSet s) {f : βα} (hf : Monotone f) :
      theorem IsLowerSet.preimage {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsLowerSet s) {f : βα} (hf : Monotone f) :
      theorem IsUpperSet.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsUpperSet s) (f : α ≃o β) :
      IsUpperSet (f '' s)
      theorem IsLowerSet.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsLowerSet s) (f : α ≃o β) :
      IsLowerSet (f '' s)
      theorem OrderEmbedding.image_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsUpperSet (Set.range e)) (a : α) :
      e '' Set.Ici a = Set.Ici (e a)
      theorem OrderEmbedding.image_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsLowerSet (Set.range e)) (a : α) :
      e '' Set.Iic a = Set.Iic (e a)
      theorem OrderEmbedding.image_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsUpperSet (Set.range e)) (a : α) :
      e '' Set.Ioi a = Set.Ioi (e a)
      theorem OrderEmbedding.image_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsLowerSet (Set.range e)) (a : α) :
      e '' Set.Iio a = Set.Iio (e a)
      @[simp]
      theorem Set.monotone_mem {α : Type u_1} [Preorder α] {s : Set α} :
      (Monotone fun (x : α) => x s) IsUpperSet s
      @[simp]
      theorem Set.antitone_mem {α : Type u_1} [Preorder α] {s : Set α} :
      (Antitone fun (x : α) => x s) IsLowerSet s
      @[simp]
      theorem isUpperSet_setOf {α : Type u_1} [Preorder α] {p : αProp} :
      IsUpperSet {a : α | p a} Monotone p
      @[simp]
      theorem isLowerSet_setOf {α : Type u_1} [Preorder α] {p : αProp} :
      IsLowerSet {a : α | p a} Antitone p
      theorem IsUpperSet.upperBounds_subset {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) :
      s.NonemptyupperBounds s s
      theorem IsLowerSet.lowerBounds_subset {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) :
      s.NonemptylowerBounds s s
      theorem IsLowerSet.top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsLowerSet s) :
      s s = Set.univ
      theorem IsUpperSet.top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) :
      s s.Nonempty
      theorem IsUpperSet.not_top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) :
      s s =
      theorem IsUpperSet.bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsUpperSet s) :
      s s = Set.univ
      theorem IsLowerSet.bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :
      s s.Nonempty
      theorem IsLowerSet.not_bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :
      s s =
      theorem IsUpperSet.not_bddAbove {α : Type u_1} [Preorder α] {s : Set α} [NoMaxOrder α] (hs : IsUpperSet s) :
      s.Nonempty¬BddAbove s
      theorem not_bddAbove_Ici {α : Type u_1} [Preorder α] (a : α) [NoMaxOrder α] :
      theorem not_bddAbove_Ioi {α : Type u_1} [Preorder α] (a : α) [NoMaxOrder α] :
      theorem IsLowerSet.not_bddBelow {α : Type u_1} [Preorder α] {s : Set α} [NoMinOrder α] (hs : IsLowerSet s) :
      s.Nonempty¬BddBelow s
      theorem not_bddBelow_Iic {α : Type u_1} [Preorder α] (a : α) [NoMinOrder α] :
      theorem not_bddBelow_Iio {α : Type u_1} [Preorder α] (a : α) [NoMinOrder α] :
      theorem isUpperSet_iff_forall_lt {α : Type u_1} [PartialOrder α] {s : Set α} :
      IsUpperSet s ∀ ⦃a b : α⦄, a < ba sb s
      theorem isLowerSet_iff_forall_lt {α : Type u_1} [PartialOrder α] {s : Set α} :
      IsLowerSet s ∀ ⦃a b : α⦄, b < aa sb s
      theorem isUpperSet_iff_Ioi_subset {α : Type u_1} [PartialOrder α] {s : Set α} :
      IsUpperSet s ∀ ⦃a : α⦄, a sSet.Ioi a s
      theorem isLowerSet_iff_Iio_subset {α : Type u_1} [PartialOrder α] {s : Set α} :
      IsLowerSet s ∀ ⦃a : α⦄, a sSet.Iio a s

      Upper/lower sets and Fibrations #

      theorem Relation.Fibration.isLowerSet_image {α : Type u_1} {β : Type u_2} {f : αβ} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f) {s : Set α} (hs : IsLowerSet s) :
      theorem IsLowerSet.image_fibration {α : Type u_1} {β : Type u_2} {f : αβ} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f) {s : Set α} (hs : IsLowerSet s) :

      Alias of Relation.Fibration.isLowerSet_image.

      theorem Relation.fibration_iff_isLowerSet_image_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [LE β] :
      Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f ∀ (x : α), IsLowerSet (f '' Set.Iic x)
      theorem Relation.fibration_iff_isLowerSet_image {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [LE β] :
      Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f ∀ (s : Set α), IsLowerSet sIsLowerSet (f '' s)
      theorem Relation.fibration_iff_image_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] (hf : Monotone f) :
      Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f ∀ (x : α), f '' Set.Iic x = Set.Iic (f x)
      theorem Relation.Fibration.isUpperSet_image {α : Type u_1} {β : Type u_2} {f : αβ} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f) {s : Set α} (hs : IsUpperSet s) :
      theorem IsUpperSet.image_fibration {α : Type u_1} {β : Type u_2} {f : αβ} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f) {s : Set α} (hs : IsUpperSet s) :

      Alias of Relation.Fibration.isUpperSet_image.

      theorem Relation.fibration_iff_isUpperSet_image_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [LE β] :
      Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f ∀ (x : α), IsUpperSet (f '' Set.Ici x)
      theorem Relation.fibration_iff_isUpperSet_image {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [LE β] :
      Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f ∀ (s : Set α), IsUpperSet sIsUpperSet (f '' s)
      theorem Relation.fibration_iff_image_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] (hf : Monotone f) :
      Relation.Fibration (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) f ∀ (x : α), f '' Set.Ici x = Set.Ici (f x)
      theorem IsUpperSet.total {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :
      s t t s
      theorem IsLowerSet.total {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :
      s t t s

      Bundled upper/lower sets #

      structure UpperSet (α : Type u_6) [LE α] :
      Type u_6

      The type of upper sets of an order.

      An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

      Instances For
        theorem UpperSet.upper' {α : Type u_6} [LE α] (self : UpperSet α) :
        IsUpperSet self.carrier

        The carrier of an UpperSet is an upper set.

        structure LowerSet (α : Type u_6) [LE α] :
        Type u_6

        The type of lower sets of an order.

        A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

        Instances For
          theorem LowerSet.lower' {α : Type u_6} [LE α] (self : LowerSet α) :
          IsLowerSet self.carrier

          The carrier of a LowerSet is a lower set.

          instance UpperSet.instSetLike {α : Type u_1} [LE α] :
          Equations
          • UpperSet.instSetLike = { coe := UpperSet.carrier, coe_injective' := }
          def UpperSet.Simps.coe {α : Type u_1} [LE α] (s : UpperSet α) :
          Set α

          See Note [custom simps projection].

          Equations
          Instances For
            theorem UpperSet.ext_iff {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :
            s = t s = t
            theorem UpperSet.ext {α : Type u_1} [LE α] {s : UpperSet α} {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
            • LowerSet.instSetLike = { coe := LowerSet.carrier, coe_injective' := }
            def LowerSet.Simps.coe {α : Type u_1} [LE α] (s : LowerSet α) :
            Set α

            See Note [custom simps projection].

            Equations
            Instances For
              theorem LowerSet.ext_iff {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :
              s = t s = t
              theorem LowerSet.ext {α : Type u_1} [LE α] {s : LowerSet α} {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

              Order #

              instance UpperSet.instSup {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instSup = { sup := fun (s t : UpperSet α) => { carrier := s t, upper' := } }
              instance UpperSet.instInf {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instInf = { inf := fun (s t : UpperSet α) => { carrier := s t, upper' := } }
              instance UpperSet.instTop {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instTop = { top := { carrier := , upper' := } }
              instance UpperSet.instBot {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instBot = { bot := { carrier := Set.univ, upper' := } }
              instance UpperSet.instSupSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instSupSet = { sSup := fun (S : Set (UpperSet α)) => { carrier := sS, s, upper' := } }
              instance UpperSet.instInfSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instInfSet = { sInf := fun (S : Set (UpperSet α)) => { carrier := sS, s, upper' := } }
              Equations
              Equations
              • One or more equations did not get rendered due to their size.
              instance UpperSet.instInhabited {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instInhabited = { default := }
              @[simp]
              theorem UpperSet.coe_subset_coe {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :
              s t t s
              @[simp]
              theorem UpperSet.coe_ssubset_coe {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :
              s t t < s
              @[simp]
              theorem UpperSet.coe_top {α : Type u_1} [LE α] :
              =
              @[simp]
              theorem UpperSet.coe_bot {α : Type u_1} [LE α] :
              = Set.univ
              @[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 : UpperSet α) (t : UpperSet α) :
              (s t) = s t
              @[simp]
              theorem UpperSet.coe_inf {α : Type u_1} [LE α] (s : UpperSet α) (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 : UpperSet α} {t : UpperSet α} {a : α} :
              a s t a s a t
              @[simp]
              theorem UpperSet.mem_inf_iff {α : Type u_1} [LE α] {s : UpperSet α} {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 : UpperSet α} {t : UpperSet α} :
              Codisjoint s t Disjoint s t
              instance LowerSet.instSup {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instSup = { sup := fun (s t : LowerSet α) => { carrier := s t, lower' := } }
              instance LowerSet.instInf {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instInf = { inf := fun (s t : LowerSet α) => { carrier := s t, lower' := } }
              instance LowerSet.instTop {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instTop = { top := { carrier := Set.univ, lower' := } }
              instance LowerSet.instBot {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instBot = { bot := { carrier := , lower' := } }
              instance LowerSet.instSupSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instSupSet = { sSup := fun (S : Set (LowerSet α)) => { carrier := sS, s, lower' := } }
              instance LowerSet.instInfSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instInfSet = { sInf := fun (S : Set (LowerSet α)) => { carrier := sS, s, lower' := } }
              Equations
              Equations
              • One or more equations did not get rendered due to their size.
              instance LowerSet.instInhabited {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instInhabited = { default := }
              theorem LowerSet.coe_subset_coe {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :
              s t s t
              theorem LowerSet.coe_ssubset_coe {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :
              s t s < t
              @[simp]
              theorem LowerSet.coe_top {α : Type u_1} [LE α] :
              = Set.univ
              @[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 : LowerSet α) (t : LowerSet α) :
              (s t) = s t
              @[simp]
              theorem LowerSet.coe_inf {α : Type u_1} [LE α] (s : LowerSet α) (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 : LowerSet α} {t : LowerSet α} {a : α} :
              a s t a s a t
              @[simp]
              theorem LowerSet.mem_inf_iff {α : Type u_1} [LE α] {s : LowerSet α} {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 : LowerSet α} {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 α) :
                  s.compl.compl = s
                  @[simp]
                  theorem UpperSet.compl_le_compl {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :
                  s.compl t.compl s t
                  @[simp]
                  theorem UpperSet.compl_sup {α : Type u_1} [LE α] (s : UpperSet α) (t : UpperSet α) :
                  (s t).compl = s.compl t.compl
                  @[simp]
                  theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s : UpperSet α) (t : UpperSet α) :
                  (s t).compl = s.compl t.compl
                  @[simp]
                  theorem UpperSet.compl_top {α : Type u_1} [LE α] :
                  .compl =
                  @[simp]
                  theorem UpperSet.compl_bot {α : Type u_1} [LE α] :
                  .compl =
                  @[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 α) :
                  s.compl.compl = s
                  @[simp]
                  theorem LowerSet.compl_le_compl {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :
                  s.compl t.compl s t
                  theorem LowerSet.compl_sup {α : Type u_1} [LE α] (s : LowerSet α) (t : LowerSet α) :
                  (s t).compl = s.compl t.compl
                  theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s : LowerSet α) (t : LowerSet α) :
                  (s t).compl = s.compl t.compl
                  theorem LowerSet.compl_top {α : Type u_1} [LE α] :
                  .compl =
                  theorem LowerSet.compl_bot {α : Type u_1} [LE α] :
                  .compl =
                  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
                  @[simp]
                  theorem upperSetIsoLowerSet_symm_apply {α : Type u_1} [LE α] (s : LowerSet α) :
                  (RelIso.symm upperSetIsoLowerSet) s = s.compl
                  @[simp]
                  theorem upperSetIsoLowerSet_apply {α : Type u_1} [LE α] (s : UpperSet α) :
                  upperSetIsoLowerSet s = s.compl
                  def upperSetIsoLowerSet {α : Type u_1} [LE α] :

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

                  Equations
                  • upperSetIsoLowerSet = { toFun := UpperSet.compl, invFun := LowerSet.compl, left_inv := , right_inv := , map_rel_iff' := }
                  Instances For
                    instance UpperSet.isTotal_le {α : Type u_1} [LinearOrder α] :
                    IsTotal (UpperSet α) fun (x1 x2 : UpperSet α) => x1 x2
                    Equations
                    • =
                    instance LowerSet.isTotal_le {α : Type u_1} [LinearOrder α] :
                    IsTotal (LowerSet α) fun (x1 x2 : LowerSet α) => x1 x2
                    Equations
                    • =
                    noncomputable instance UpperSet.instLinearOrder {α : Type u_1} [LinearOrder α] :
                    Equations
                    noncomputable instance LowerSet.instLinearOrder {α : Type u_1} [LinearOrder α] :
                    Equations
                    Equations
                    • UpperSet.instCompleteLinearOrder = CompleteLinearOrder.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
                    Equations
                    • LowerSet.instCompleteLinearOrder = CompleteLinearOrder.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT

                    Map #

                    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 β) :
                      (UpperSet.map f).symm = UpperSet.map f.symm
                      @[simp]
                      theorem UpperSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α ≃o β} {s : UpperSet α} {b : β} :
                      b (UpperSet.map f) s f.symm b s
                      @[simp]
                      theorem UpperSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : UpperSet α} (g : β ≃o γ) (f : α ≃o β) :
                      (UpperSet.map g) ((UpperSet.map f) s) = (UpperSet.map (f.trans g)) s
                      @[simp]
                      theorem UpperSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) :
                      ((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 β) :
                        (LowerSet.map f).symm = LowerSet.map f.symm
                        @[simp]
                        theorem LowerSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {f : α ≃o β} {b : β} :
                        b (LowerSet.map f) s f.symm b s
                        @[simp]
                        theorem LowerSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : LowerSet α} (g : β ≃o γ) (f : α ≃o β) :
                        (LowerSet.map g) ((LowerSet.map f) s) = (LowerSet.map (f.trans g)) s
                        @[simp]
                        theorem LowerSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) :
                        ((LowerSet.map f) s) = f '' s
                        @[simp]
                        theorem UpperSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) :
                        ((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 α) :
                        ((LowerSet.map f) s).compl = (UpperSet.map f) s.compl

                        Principal sets #

                        def UpperSet.Ici {α : Type u_1} [Preorder α] (a : α) :

                        The smallest upper set containing a given element.

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

                          The smallest upper set containing a given element.

                          Equations
                          Instances For
                            @[simp]
                            theorem UpperSet.coe_Ici {α : Type u_1} [Preorder α] (a : α) :
                            @[simp]
                            theorem UpperSet.coe_Ioi {α : Type u_1} [Preorder α] (a : α) :
                            @[simp]
                            theorem UpperSet.mem_Ici_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
                            @[simp]
                            theorem UpperSet.mem_Ioi_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
                            @[simp]
                            theorem UpperSet.map_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                            @[simp]
                            theorem UpperSet.map_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                            theorem UpperSet.Ici_le_Ioi {α : Type u_1} [Preorder α] (a : α) :
                            @[simp]
                            theorem UpperSet.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :
                            @[simp]
                            theorem UpperSet.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] :
                            @[simp]
                            theorem UpperSet.Ici_ne_top {α : Type u_1} [Preorder α] {a : α} :
                            @[simp]
                            theorem UpperSet.Ici_lt_top {α : Type u_1} [Preorder α] {a : α} :
                            @[simp]
                            theorem UpperSet.le_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :
                            @[simp]
                            theorem UpperSet.Ici_inj {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
                            theorem UpperSet.Ici_ne_Ici {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
                            @[simp]
                            theorem UpperSet.Ici_sup {α : Type u_1} [SemilatticeSup α] (a : α) (b : α) :
                            @[simp]
                            theorem UpperSet.Ici_sSup {α : Type u_1} [CompleteLattice α] (S : Set α) :
                            UpperSet.Ici (sSup S) = aS, UpperSet.Ici a
                            @[simp]
                            theorem UpperSet.Ici_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) :
                            UpperSet.Ici (⨆ (i : ι), f i) = ⨆ (i : ι), UpperSet.Ici (f i)
                            theorem UpperSet.Ici_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [CompleteLattice α] (f : (i : ι) → κ iα) :
                            UpperSet.Ici (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), UpperSet.Ici (f i j)
                            def LowerSet.Iic {α : Type u_1} [Preorder α] (a : α) :

                            Principal lower set. Set.Iic as a lower set. The smallest lower set containing a given element.

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

                              Strict principal lower set. Set.Iio as a lower set.

                              Equations
                              Instances For
                                @[simp]
                                theorem LowerSet.coe_Iic {α : Type u_1} [Preorder α] (a : α) :
                                @[simp]
                                theorem LowerSet.coe_Iio {α : Type u_1} [Preorder α] (a : α) :
                                @[simp]
                                theorem LowerSet.mem_Iic_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
                                @[simp]
                                theorem LowerSet.mem_Iio_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
                                @[simp]
                                theorem LowerSet.map_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                                @[simp]
                                theorem LowerSet.map_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :
                                theorem LowerSet.Ioi_le_Ici {α : Type u_1} [Preorder α] (a : α) :
                                @[simp]
                                theorem LowerSet.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] :
                                @[simp]
                                theorem LowerSet.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] :
                                @[simp]
                                theorem LowerSet.Iic_ne_bot {α : Type u_1} [Preorder α] {a : α} :
                                @[simp]
                                theorem LowerSet.bot_lt_Iic {α : Type u_1} [Preorder α] {a : α} :
                                @[simp]
                                theorem LowerSet.Iic_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :
                                @[simp]
                                theorem LowerSet.Iic_inj {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
                                theorem LowerSet.Iic_ne_Iic {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
                                @[simp]
                                theorem LowerSet.Iic_inf {α : Type u_1} [SemilatticeInf α] (a : α) (b : α) :
                                @[simp]
                                theorem LowerSet.Iic_sInf {α : Type u_1} [CompleteLattice α] (S : Set α) :
                                LowerSet.Iic (sInf S) = aS, LowerSet.Iic a
                                @[simp]
                                theorem LowerSet.Iic_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) :
                                LowerSet.Iic (⨅ (i : ι), f i) = ⨅ (i : ι), LowerSet.Iic (f i)
                                theorem LowerSet.Iic_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [CompleteLattice α] (f : (i : ι) → κ iα) :
                                LowerSet.Iic (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), LowerSet.Iic (f i j)
                                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
                                    • instDecidablePredMemUpperClosure = inst
                                    instance instDecidablePredMemLowerClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun (x : α) => as, x a] :
                                    DecidablePred fun (x : α) => x lowerClosure s
                                    Equations
                                    • instDecidablePredMemLowerClosure = inst
                                    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 : Set α} {t : Set α} (h : s t) (ht : IsUpperSet t) :
                                    (upperClosure s) t
                                    theorem lowerClosure_min {α : Type u_1} [Preorder α] {s : Set α} {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, UpperSet.Ici a = upperClosure s
                                    @[simp]
                                    theorem LowerSet.iSup_Iic {α : Type u_1} [Preorder α] (s : Set α) :
                                    as, LowerSet.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
                                    theorem gc_upperClosure_coe {α : Type u_1} [Preorder α] :
                                    GaloisConnection (OrderDual.toDual upperClosure) (SetLike.coe OrderDual.ofDual)
                                    theorem gc_lowerClosure_coe {α : Type u_1} [Preorder α] :
                                    GaloisConnection lowerClosure SetLike.coe
                                    def giUpperClosureCoe {α : Type u_1} [Preorder α] :
                                    GaloisInsertion (OrderDual.toDual upperClosure) (SetLike.coe OrderDual.ofDual)

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def giLowerClosureCoe {α : Type u_1} [Preorder α] :
                                      GaloisInsertion lowerClosure SetLike.coe

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

                                      Equations
                                      • giLowerClosureCoe = { choice := fun (s : Set α) (hs : (lowerClosure s) s) => { carrier := s, lower' := }, gc := , le_l_u := , choice_eq := }
                                      Instances For
                                        theorem upperClosure_anti {α : Type u_1} [Preorder α] :
                                        Antitone upperClosure
                                        theorem lowerClosure_mono {α : Type u_1} [Preorder α] :
                                        Monotone lowerClosure
                                        @[simp]
                                        @[simp]
                                        @[simp]
                                        theorem upperClosure_singleton {α : Type u_1} [Preorder α] (a : α) :
                                        @[simp]
                                        theorem lowerClosure_singleton {α : Type u_1} [Preorder α] (a : α) :
                                        @[simp]
                                        theorem upperClosure_univ {α : Type u_1} [Preorder α] :
                                        upperClosure Set.univ =
                                        @[simp]
                                        theorem lowerClosure_univ {α : Type u_1} [Preorder α] :
                                        lowerClosure Set.univ =
                                        @[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 : Set α) (t : Set α) :
                                        @[simp]
                                        theorem lowerClosure_union {α : Type u_1} [Preorder α] (s : Set α) (t : Set α) :
                                        @[simp]
                                        theorem upperClosure_iUnion {α : Type u_1} {ι : Sort u_4} [Preorder α] (f : ιSet α) :
                                        upperClosure (⋃ (i : ι), f i) = ⨅ (i : ι), upperClosure (f i)
                                        @[simp]
                                        theorem lowerClosure_iUnion {α : Type u_1} {ι : Sort u_4} [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
                                        theorem Set.OrdConnected.upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} (h : s.OrdConnected) :
                                        (upperClosure s) (lowerClosure s) = s
                                        theorem ordConnected_iff_upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :
                                        s.OrdConnected (upperClosure s) (lowerClosure s) = 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.of_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

                                        Alias of the forward direction of bddAbove_lowerClosure.

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

                                        Alias of the reverse direction of bddAbove_lowerClosure.

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

                                        Alias of the reverse direction of bddBelow_upperClosure.

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

                                        Alias of the forward direction of bddBelow_upperClosure.

                                        @[simp]
                                        theorem IsLowerSet.disjoint_upperClosure_left {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (ht : IsLowerSet t) :
                                        @[simp]
                                        theorem IsLowerSet.disjoint_upperClosure_right {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (hs : IsLowerSet s) :
                                        @[simp]
                                        theorem IsUpperSet.disjoint_lowerClosure_left {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (ht : IsUpperSet t) :
                                        @[simp]
                                        theorem IsUpperSet.disjoint_lowerClosure_right {α : Type u_1} [Preorder α] {s : Set α} {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 α} :

                                        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 t lowerClosure 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 t s.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 a LowerSet.Iic a = s
                                            theorem LowerSet.Iic_sup_erase {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a s) (has : bs, a bb = a) :
                                            LowerSet.Iic a s.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 t upperClosure 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 t s.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 a UpperSet.Ici a = s
                                                theorem UpperSet.Ici_inf_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a s) (has : bs, b ab = a) :
                                                UpperSet.Ici a s.erase a = s

                                                Product #

                                                theorem IsUpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsUpperSet s) (ht : IsUpperSet t) :
                                                theorem IsLowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsLowerSet s) (ht : IsLowerSet t) :
                                                def UpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :
                                                UpperSet (α × β)

                                                The product of two upper sets as an upper set.

                                                Equations
                                                • s.prod t = { carrier := s ×ˢ t, upper' := }
                                                Instances For
                                                  instance UpperSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                                                  SProd (UpperSet α) (UpperSet β) (UpperSet (α × β))
                                                  Equations
                                                  • UpperSet.instSProd = { sprod := UpperSet.prod }
                                                  @[simp]
                                                  theorem UpperSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :
                                                  (s ×ˢ t) = s ×ˢ t
                                                  @[simp]
                                                  theorem UpperSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : UpperSet α} {t : UpperSet β} :
                                                  x s ×ˢ t x.1 s x.2 t
                                                  theorem UpperSet.Ici_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :
                                                  @[simp]
                                                  theorem UpperSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
                                                  @[simp]
                                                  theorem UpperSet.prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) :
                                                  @[simp]
                                                  theorem UpperSet.top_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : UpperSet β) :
                                                  @[simp]
                                                  theorem UpperSet.bot_prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                                                  @[simp]
                                                  theorem UpperSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : UpperSet α) (s₂ : UpperSet α) (t : UpperSet β) :
                                                  (s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
                                                  @[simp]
                                                  theorem UpperSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ : UpperSet β) (t₂ : UpperSet β) :
                                                  s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
                                                  @[simp]
                                                  theorem UpperSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : UpperSet α) (s₂ : UpperSet α) (t : UpperSet β) :
                                                  (s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
                                                  @[simp]
                                                  theorem UpperSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ : UpperSet β) (t₂ : UpperSet β) :
                                                  s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
                                                  theorem UpperSet.prod_sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : UpperSet α) (s₂ : UpperSet α) (t₁ : UpperSet β) (t₂ : UpperSet β) :
                                                  s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
                                                  theorem UpperSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :
                                                  s₁ s₂t₁ t₂s₁ ×ˢ t₁ s₂ ×ˢ t₂
                                                  theorem UpperSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t : UpperSet β} :
                                                  s₁ s₂s₁ ×ˢ t s₂ ×ˢ t
                                                  theorem UpperSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :
                                                  t₁ t₂s ×ˢ t₁ s ×ˢ t₂
                                                  @[simp]
                                                  theorem UpperSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ : UpperSet α} {s₂ : UpperSet α} :
                                                  s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
                                                  @[simp]
                                                  theorem UpperSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ : UpperSet α} {s₂ : UpperSet α} :
                                                  s₁ ×ˢ s₁ < s₂ ×ˢ s₂ s₁ < s₂
                                                  theorem UpperSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :
                                                  s₁ ×ˢ t₁ s₂ ×ˢ t₂ s₁ s₂ t₁ t₂ s₂ = t₂ =
                                                  @[simp]
                                                  theorem UpperSet.prod_eq_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t : UpperSet β} :
                                                  s ×ˢ t = s = t =
                                                  @[simp]
                                                  theorem UpperSet.codisjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :
                                                  Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) Codisjoint s₁ s₂ Codisjoint t₁ t₂
                                                  def LowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :
                                                  LowerSet (α × β)

                                                  The product of two lower sets as a lower set.

                                                  Equations
                                                  • s.prod t = { carrier := s ×ˢ t, lower' := }
                                                  Instances For
                                                    instance LowerSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                                                    SProd (LowerSet α) (LowerSet β) (LowerSet (α × β))
                                                    Equations
                                                    • LowerSet.instSProd = { sprod := LowerSet.prod }
                                                    @[simp]
                                                    theorem LowerSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :
                                                    (s ×ˢ t) = s ×ˢ t
                                                    @[simp]
                                                    theorem LowerSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : LowerSet α} {t : LowerSet β} :
                                                    x s ×ˢ t x.1 s x.2 t
                                                    theorem LowerSet.Iic_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :
                                                    @[simp]
                                                    theorem LowerSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :
                                                    @[simp]
                                                    theorem LowerSet.prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) :
                                                    @[simp]
                                                    theorem LowerSet.bot_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : LowerSet β) :
                                                    @[simp]
                                                    theorem LowerSet.top_prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                                                    @[simp]
                                                    theorem LowerSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : LowerSet α) (s₂ : LowerSet α) (t : LowerSet β) :
                                                    (s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
                                                    @[simp]
                                                    theorem LowerSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ : LowerSet β) (t₂ : LowerSet β) :
                                                    s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
                                                    @[simp]
                                                    theorem LowerSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : LowerSet α) (s₂ : LowerSet α) (t : LowerSet β) :
                                                    (s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
                                                    @[simp]
                                                    theorem LowerSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ : LowerSet β) (t₂ : LowerSet β) :
                                                    s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
                                                    theorem LowerSet.prod_inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : LowerSet α) (s₂ : LowerSet α) (t₁ : LowerSet β) (t₂ : LowerSet β) :
                                                    s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
                                                    theorem LowerSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :
                                                    s₁ s₂t₁ t₂s₁ ×ˢ t₁ s₂ ×ˢ t₂
                                                    theorem LowerSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t : LowerSet β} :
                                                    s₁ s₂s₁ ×ˢ t s₂ ×ˢ t
                                                    theorem LowerSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :
                                                    t₁ t₂s ×ˢ t₁ s ×ˢ t₂
                                                    @[simp]
                                                    theorem LowerSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ : LowerSet α} {s₂ : LowerSet α} :
                                                    s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
                                                    @[simp]
                                                    theorem LowerSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ : LowerSet α} {s₂ : LowerSet α} :
                                                    s₁ ×ˢ s₁ < s₂ ×ˢ s₂ s₁ < s₂
                                                    theorem LowerSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :
                                                    s₁ ×ˢ t₁ s₂ ×ˢ t₂ s₁ s₂ t₁ t₂ s₁ = t₁ =
                                                    @[simp]
                                                    theorem LowerSet.prod_eq_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t : LowerSet β} :
                                                    s ×ˢ t = s = t =
                                                    @[simp]
                                                    theorem LowerSet.disjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :
                                                    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) Disjoint s₁ s₂ Disjoint t₁ t₂
                                                    @[simp]
                                                    theorem upperClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :
                                                    @[simp]
                                                    theorem lowerClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :