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 : ∀ (s : Set α), s SIsUpperSet s) :
      theorem isLowerSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ (s : Set α), s SIsLowerSet 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 : ∀ (s : Set α), s SIsUpperSet s) :
      theorem isLowerSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ (s : Set α), s SIsLowerSet 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_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.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) :
      theorem IsLowerSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) :
      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)
      @[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 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) :
      theorem IsUpperSet.not_top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet 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) :
      theorem IsLowerSet.not_bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :
      theorem IsUpperSet.not_bddAbove {α : Type u_1} [Preorder α] {s : Set α} [NoMaxOrder α] (hs : IsUpperSet 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) :
      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
      theorem IsUpperSet.Ioi_subset {α : Type u_1} [PartialOrder α] {s : Set α} :
      IsUpperSet s∀ ⦃a : α⦄, a sSet.Ioi a s

      Alias of the forward direction of isUpperSet_iff_Ioi_subset.

      theorem IsLowerSet.Iio_subset {α : Type u_1} [PartialOrder α] {s : Set α} :
      IsLowerSet s∀ ⦃a : α⦄, a sSet.Iio a s

      Alias of the forward direction of isLowerSet_iff_Iio_subset.

      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.

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

        The type of lower sets of an order.

        Instances For
          instance UpperSet.instSetLikeUpperSet {α : Type u_1} [LE α] :
          Equations
          • UpperSet.instSetLikeUpperSet = { coe := UpperSet.carrier, coe_injective' := (_ : ∀ (s t : UpperSet α), s.carrier = t.carriers = t) }
          theorem UpperSet.ext {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :
          s = ts = t
          def UpperSet.Simps.coe {α : Type u_1} [LE α] (s : UpperSet α) :
          Set α

          See Note [custom simps projection].

          Equations
          Instances For
            @[simp]
            theorem UpperSet.carrier_eq_coe {α : Type u_1} [LE α] (s : UpperSet α) :
            s.carrier = s
            theorem UpperSet.upper {α : Type u_1} [LE α] (s : UpperSet α) :
            @[simp]
            theorem UpperSet.mem_mk {α : Type u_1} [LE α] (carrier : Set α) (upper' : IsUpperSet carrier) {a : α} :
            a { carrier := carrier, upper' := upper' } a carrier
            instance LowerSet.instSetLikeLowerSet {α : Type u_1} [LE α] :
            Equations
            • LowerSet.instSetLikeLowerSet = { coe := LowerSet.carrier, coe_injective' := (_ : ∀ (s t : LowerSet α), s.carrier = t.carriers = t) }
            def LowerSet.Simps.coe {α : Type u_1} [LE α] (s : LowerSet α) :
            Set α

            See Note [custom simps projection].

            Equations
            Instances For
              theorem LowerSet.ext {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :
              s = ts = t
              @[simp]
              theorem LowerSet.carrier_eq_coe {α : Type u_1} [LE α] (s : LowerSet α) :
              s.carrier = s
              theorem LowerSet.lower {α : Type u_1} [LE α] (s : LowerSet α) :
              @[simp]
              theorem LowerSet.mem_mk {α : Type u_1} [LE α] (carrier : Set α) (lower' : IsLowerSet carrier) {a : α} :
              a { carrier := carrier, lower' := lower' } a carrier

              Order #

              instance UpperSet.instSupUpperSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instSupUpperSet = { sup := fun s t => { carrier := s t, upper' := (_ : IsUpperSet (s t)) } }
              instance UpperSet.instInfUpperSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instInfUpperSet = { inf := fun s t => { carrier := s t, upper' := (_ : IsUpperSet (s t)) } }
              instance UpperSet.instTopUpperSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instTopUpperSet = { top := { carrier := , upper' := (_ : IsUpperSet ) } }
              instance UpperSet.instBotUpperSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instBotUpperSet = { bot := { carrier := Set.univ, upper' := (_ : IsUpperSet Set.univ) } }
              instance UpperSet.instSupSetUpperSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instSupSetUpperSet = { sSup := fun S => { carrier := ⋂ (s : UpperSet α) (_ : s S), s, upper' := (_ : IsUpperSet (⋂ (i : UpperSet α) (_ : i S), i)) } }
              instance UpperSet.instInfSetUpperSet {α : Type u_1} [LE α] :
              Equations
              • UpperSet.instInfSetUpperSet = { sInf := fun S => { carrier := ⋃ (s : UpperSet α) (_ : s S), s, upper' := (_ : IsUpperSet (⋃ (i : UpperSet α) (_ : i S), i)) } }
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • UpperSet.instInhabitedUpperSet = { default := }
              @[simp]
              theorem UpperSet.coe_subset_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_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) = ⋂ (s : UpperSet α) (_ : s S), s
              @[simp]
              theorem UpperSet.coe_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) :
              ↑(sInf S) = ⋃ (s : UpperSet α) (_ : s S), 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 : α} :
              @[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 ∀ (s : UpperSet α), s Sa s
              @[simp]
              theorem UpperSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} :
              a sInf S s, s S 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, 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.instSupLowerSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instSupLowerSet = { sup := fun s t => { carrier := s t, lower' := (_ : ∀ (x x_1 : α), x_1 xx s x tx_1 s x_1 t) } }
              instance LowerSet.instInfLowerSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instInfLowerSet = { inf := fun s t => { carrier := s t, lower' := (_ : ∀ (x x_1 : α), x_1 xx s x tx_1 s x_1 t) } }
              instance LowerSet.instTopLowerSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instTopLowerSet = { top := { carrier := Set.univ, lower' := (_ : ∀ (x x_1 : α), x_1 xx Set.univx Set.univ) } }
              instance LowerSet.instBotLowerSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instBotLowerSet = { bot := { carrier := , lower' := (_ : ∀ (x x_1 : α), x_1 xx x ) } }
              instance LowerSet.instSupSetLowerSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instSupSetLowerSet = { sSup := fun S => { carrier := ⋃ (s : LowerSet α) (_ : s S), s, lower' := (_ : IsLowerSet (⋃ (i : LowerSet α) (_ : i S), i)) } }
              instance LowerSet.instInfSetLowerSet {α : Type u_1} [LE α] :
              Equations
              • LowerSet.instInfSetLowerSet = { sInf := fun S => { carrier := ⋂ (s : LowerSet α) (_ : s S), s, lower' := (_ : IsLowerSet (⋂ (i : LowerSet α) (_ : i S), i)) } }
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • LowerSet.instInhabitedLowerSet = { default := }
              theorem LowerSet.coe_subset_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_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) = ⋃ (s : LowerSet α) (_ : s S), s
              @[simp]
              theorem LowerSet.coe_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) :
              ↑(sInf S) = ⋂ (s : LowerSet α) (_ : s S), 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 : α} :
              @[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 s, s S a s
              @[simp]
              theorem LowerSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} :
              a sInf S ∀ (s : LowerSet α), s Sa 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, 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
              Instances For
                def LowerSet.compl {α : Type u_1} [LE α] (s : LowerSet α) :

                The complement of a lower set as an upper set.

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

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • One or more equations did not get rendered due to their size.

                    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 β) :
                      @[simp]
                      theorem UpperSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α ≃o β} {s : UpperSet α} {b : β} :
                      b ↑(UpperSet.map f) s ↑(OrderIso.symm f) 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 (OrderIso.trans f 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 β) :
                        @[simp]
                        theorem LowerSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {f : α ≃o β} {b : β} :
                        b ↑(LowerSet.map f) s ↑(OrderIso.symm f) 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 (OrderIso.trans f 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 α) :
                        @[simp]
                        theorem LowerSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) :

                        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.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] :
                            @[simp]
                            theorem UpperSet.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :
                            @[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) = ⨆ (a : α) (_ : a S), 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_inf {α : Type u_1} [SemilatticeInf α] (a : α) (b : α) :
                                @[simp]
                                theorem LowerSet.Iic_sInf {α : Type u_1} [CompleteLattice α] (S : Set α) :
                                LowerSet.Iic (sInf S) = ⨅ (a : α) (_ : a S), 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 a, a s a x
                                    @[simp]
                                    theorem mem_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} :
                                    x lowerClosure s a, a s x a
                                    theorem coe_upperClosure {α : Type u_1} [Preorder α] (s : Set α) :
                                    ↑(upperClosure s) = ⋃ (a : α) (_ : a s), Set.Ici a
                                    theorem coe_lowerClosure {α : Type u_1} [Preorder α] (s : Set α) :
                                    ↑(lowerClosure s) = ⋃ (a : α) (_ : a s), Set.Iic a
                                    instance instDecidablePredMemUpperClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun x => a, a s a x] :
                                    Equations
                                    • instDecidablePredMemUpperClosure = inst
                                    instance instDecidablePredMemLowerClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun x => a, a s x a] :
                                    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 α) :
                                    ⨅ (a : α) (_ : a s), UpperSet.Ici a = upperClosure s
                                    @[simp]
                                    theorem LowerSet.iSup_Iic {α : Type u_1} [Preorder α] (s : Set α) :
                                    ⨆ (a : α) (_ : a s), LowerSet.Iic a = lowerClosure 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
                                      • One or more equations did not get rendered due to their size.
                                      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) = ⨅ (s : Set α) (_ : s S), upperClosure s
                                        @[simp]
                                        theorem lowerClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) :
                                        lowerClosure (⋃₀ S) = ⨆ (s : Set α) (_ : s S), 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.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.

                                        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
                                        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.fst s x.snd 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
                                          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.fst s x.snd 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 β) :