# Up-sets and down-sets #

This file defines upper and lower sets in an order.

## Main declarations #

• IsUpperSet: Predicate for a set to be an upper set. This means every element greater than a member of the set is in the set itself.
• IsLowerSet: Predicate for a set to be a lower set. This means every element less than a member of the set is in the set itself.
• UpperSet: The type of upper sets.
• LowerSet: The type of lower sets.
• upperClosure: The greatest upper set containing a set.
• lowerClosure: The least lower set containing a set.
• UpperSet.Ici: Principal upper set. Set.Ici as an upper set.
• UpperSet.Ioi: Strict principal upper set. Set.Ioi as an upper set.
• LowerSet.Iic: Principal lower set. Set.Iic as a lower set.
• LowerSet.Iio: Strict principal lower set. Set.Iio as a lower set.

## Notation #

• ×ˢ is notation for UpperSet.prod / LowerSet.prod.

## 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
• = ∀ ⦃a b : α⦄, a ba sb s
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
• = ∀ ⦃a b : α⦄, b aa sb s
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 : ) :
theorem IsLowerSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : ) :
@[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 : ) (ht : ) :
theorem IsLowerSet.union {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem IsUpperSet.inter {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem IsLowerSet.inter {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem isUpperSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, ) :
theorem isLowerSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, ) :
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, ) :
theorem isLowerSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, ) :
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)
@[simp]
theorem isUpperSet_preimage_ofDual_iff {α : Type u_1} [LE α] {s : Set α} :
IsUpperSet (OrderDual.ofDual ⁻¹' s)
@[simp]
theorem isLowerSet_preimage_toDual_iff {α : Type u_1} [LE α] {s : } :
IsLowerSet (OrderDual.toDual ⁻¹' s)
@[simp]
theorem isUpperSet_preimage_toDual_iff {α : Type u_1} [LE α] {s : } :
IsUpperSet (OrderDual.toDual ⁻¹' s)
theorem IsUpperSet.toDual {α : Type u_1} [LE α] {s : Set α} :
IsLowerSet (OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of isLowerSet_preimage_ofDual_iff.

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

Alias of the reverse direction of isUpperSet_preimage_ofDual_iff.

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

Alias of the reverse direction of isLowerSet_preimage_toDual_iff.

theorem IsLowerSet.ofDual {α : Type u_1} [LE α] {s : } :
IsUpperSet (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 : ) :
IsLowerSet (Subtype.val ⁻¹' t) bs, ct, b cb t
theorem IsLowerSet.isUpperSet_preimage_coe {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) :
IsUpperSet (Subtype.val ⁻¹' t) bs, ct, c bb t
theorem IsUpperSet.sdiff {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : bs, ct, b cb t) :
theorem IsLowerSet.sdiff {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : bs, ct, c bb t) :
theorem IsUpperSet.sdiff_of_isLowerSet {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem IsLowerSet.sdiff_of_isUpperSet {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem IsUpperSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : ) (has : bs, b ab = a) :
IsUpperSet (s \ {a})
theorem IsLowerSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : ) (has : bs, a bb = a) :
IsLowerSet (s \ {a})
theorem isUpperSet_Ici {α : Type u_1} [] (a : α) :
theorem isLowerSet_Iic {α : Type u_1} [] (a : α) :
theorem isUpperSet_Ioi {α : Type u_1} [] (a : α) :
theorem isLowerSet_Iio {α : Type u_1} [] (a : α) :
theorem isUpperSet_iff_Ici_subset {α : Type u_1} [] {s : Set α} :
∀ ⦃a : α⦄, a s s
theorem isLowerSet_iff_Iic_subset {α : Type u_1} [] {s : Set α} :
∀ ⦃a : α⦄, a s s
theorem IsUpperSet.Ici_subset {α : Type u_1} [] {s : Set α} :
∀ ⦃a : α⦄, a s s

Alias of the forward direction of isUpperSet_iff_Ici_subset.

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

Alias of the forward direction of isLowerSet_iff_Iic_subset.

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

• carrier : Set α

The carrier of an UpperSet.

• upper' : IsUpperSet self.carrier

The carrier of an UpperSet is an upper set.

Instances For
theorem UpperSet.upper' {α : Type u_6} [LE α] (self : ) :
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.

• carrier : Set α

The carrier of a LowerSet.

• lower' : IsLowerSet self.carrier

The carrier of a LowerSet is a lower set.

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

The carrier of a LowerSet is a lower set.

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

See Note [custom simps projection].

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

See Note [custom simps projection].

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

#### Order #

instance UpperSet.instSup {α : Type u_1} [LE α] :
Sup ()
Equations
• UpperSet.instSup = { sup := fun (s t : ) => { carrier := s t, upper' := } }
instance UpperSet.instInf {α : Type u_1} [LE α] :
Inf ()
Equations
• UpperSet.instInf = { inf := fun (s t : ) => { carrier := s t, upper' := } }
instance UpperSet.instTop {α : Type u_1} [LE α] :
Top ()
Equations
• UpperSet.instTop = { top := { carrier := , upper' := } }
instance UpperSet.instBot {α : Type u_1} [LE α] :
Bot ()
Equations
• UpperSet.instBot = { bot := { carrier := Set.univ, upper' := } }
instance UpperSet.instSupSet {α : Type u_1} [LE α] :
Equations
• UpperSet.instSupSet = { sSup := fun (S : Set ()) => { carrier := sS, s, upper' := } }
instance UpperSet.instInfSet {α : Type u_1} [LE α] :
Equations
• UpperSet.instInfSet = { sInf := fun (S : Set ()) => { carrier := sS, s, upper' := } }
instance UpperSet.completelyDistribLattice {α : Type u_1} [LE α] :
Equations
instance UpperSet.instInhabited {α : Type u_1} [LE α] :
Equations
• UpperSet.instInhabited = { default := }
@[simp]
theorem UpperSet.coe_subset_coe {α : Type u_1} [LE α] {s : } {t : } :
s t t s
@[simp]
theorem UpperSet.coe_ssubset_coe {α : Type u_1} [LE α] {s : } {t : } :
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 : } :
s = Set.univ s =
@[simp]
theorem UpperSet.coe_eq_empty {α : Type u_1} [LE α] {s : } :
s = s =
@[simp]
theorem UpperSet.coe_nonempty {α : Type u_1} [LE α] {s : } :
(s).Nonempty s
@[simp]
theorem UpperSet.coe_sup {α : Type u_1} [LE α] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem UpperSet.coe_inf {α : Type u_1} [LE α] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem UpperSet.coe_sSup {α : Type u_1} [LE α] (S : Set ()) :
(sSup S) = sS, s
@[simp]
theorem UpperSet.coe_sInf {α : Type u_1} [LE α] (S : Set ()) :
(sInf S) = sS, s
@[simp]
theorem UpperSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨆ (i : ι), f i) = ⋂ (i : ι), (f i)
@[simp]
theorem UpperSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨅ (i : ι), f i) = ⋃ (i : ι), (f i)
theorem UpperSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ i) :
(⨆ (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 : ι) → κ i) :
(⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), (f i j)
@[simp]
theorem UpperSet.not_mem_top {α : Type u_1} [LE α] {a : α} :
a
@[simp]
theorem UpperSet.mem_bot {α : Type u_1} [LE α] {a : α} :
@[simp]
theorem UpperSet.mem_sup_iff {α : Type u_1} [LE α] {s : } {t : } {a : α} :
a s t a s a t
@[simp]
theorem UpperSet.mem_inf_iff {α : Type u_1} [LE α] {s : } {t : } {a : α} :
a s t a s a t
@[simp]
theorem UpperSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set ()} {a : α} :
a sSup S sS, a s
@[simp]
theorem UpperSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set ()} {a : α} :
a sInf S sS, a s
@[simp]
theorem UpperSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι} :
a ⨆ (i : ι), f i ∀ (i : ι), a f i
@[simp]
theorem UpperSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι} :
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 : ι) → κ i} :
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 : ι) → κ i} :
a ⨅ (i : ι), ⨅ (j : κ i), f i j ∃ (i : ι) (j : κ i), a f i j
@[simp]
theorem UpperSet.codisjoint_coe {α : Type u_1} [LE α] {s : } {t : } :
Codisjoint s t Disjoint s t
instance LowerSet.instSup {α : Type u_1} [LE α] :
Sup ()
Equations
• LowerSet.instSup = { sup := fun (s t : ) => { carrier := s t, lower' := } }
instance LowerSet.instInf {α : Type u_1} [LE α] :
Inf ()
Equations
• LowerSet.instInf = { inf := fun (s t : ) => { carrier := s t, lower' := } }
instance LowerSet.instTop {α : Type u_1} [LE α] :
Top ()
Equations
• LowerSet.instTop = { top := { carrier := Set.univ, lower' := } }
instance LowerSet.instBot {α : Type u_1} [LE α] :
Bot ()
Equations
• LowerSet.instBot = { bot := { carrier := , lower' := } }
instance LowerSet.instSupSet {α : Type u_1} [LE α] :
Equations
• LowerSet.instSupSet = { sSup := fun (S : Set ()) => { carrier := sS, s, lower' := } }
instance LowerSet.instInfSet {α : Type u_1} [LE α] :
Equations
• LowerSet.instInfSet = { sInf := fun (S : Set ()) => { carrier := sS, s, lower' := } }
instance LowerSet.completelyDistribLattice {α : Type u_1} [LE α] :
Equations
instance LowerSet.instInhabited {α : Type u_1} [LE α] :
Equations
• LowerSet.instInhabited = { default := }
theorem LowerSet.coe_subset_coe {α : Type u_1} [LE α] {s : } {t : } :
s t s t
theorem LowerSet.coe_ssubset_coe {α : Type u_1} [LE α] {s : } {t : } :
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 : } :
s = Set.univ s =
@[simp]
theorem LowerSet.coe_eq_empty {α : Type u_1} [LE α] {s : } :
s = s =
@[simp]
theorem LowerSet.coe_nonempty {α : Type u_1} [LE α] {s : } :
(s).Nonempty s
@[simp]
theorem LowerSet.coe_sup {α : Type u_1} [LE α] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem LowerSet.coe_inf {α : Type u_1} [LE α] (s : ) (t : ) :
(s t) = s t
@[simp]
theorem LowerSet.coe_sSup {α : Type u_1} [LE α] (S : Set ()) :
(sSup S) = sS, s
@[simp]
theorem LowerSet.coe_sInf {α : Type u_1} [LE α] (S : Set ()) :
(sInf S) = sS, s
@[simp]
theorem LowerSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨆ (i : ι), f i) = ⋃ (i : ι), (f i)
@[simp]
theorem LowerSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
theorem LowerSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ i) :
(⨆ (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 : ι) → κ i) :
(⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), (f i j)
@[simp]
theorem LowerSet.mem_top {α : Type u_1} [LE α] {a : α} :
@[simp]
theorem LowerSet.not_mem_bot {α : Type u_1} [LE α] {a : α} :
a
@[simp]
theorem LowerSet.mem_sup_iff {α : Type u_1} [LE α] {s : } {t : } {a : α} :
a s t a s a t
@[simp]
theorem LowerSet.mem_inf_iff {α : Type u_1} [LE α] {s : } {t : } {a : α} :
a s t a s a t
@[simp]
theorem LowerSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set ()} {a : α} :
a sSup S sS, a s
@[simp]
theorem LowerSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set ()} {a : α} :
a sInf S sS, a s
@[simp]
theorem LowerSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι} :
a ⨆ (i : ι), f i ∃ (i : ι), a f i
@[simp]
theorem LowerSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι} :
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 : ι) → κ i} :
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 : ι) → κ i} :
a ⨅ (i : ι), ⨅ (j : κ i), f i j ∀ (i : ι) (j : κ i), a f i j
@[simp]
theorem LowerSet.disjoint_coe {α : Type u_1} [LE α] {s : } {t : } :
Disjoint s t Disjoint s t

#### Complement #

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

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 : ) :

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 : ) :
s.compl = (s)
@[simp]
theorem UpperSet.mem_compl_iff {α : Type u_1} [LE α] {s : } {a : α} :
a s.compl as
@[simp]
theorem UpperSet.compl_compl {α : Type u_1} [LE α] (s : ) :
s.compl.compl = s
@[simp]
theorem UpperSet.compl_le_compl {α : Type u_1} [LE α] {s : } {t : } :
s.compl t.compl s t
@[simp]
theorem UpperSet.compl_sup {α : Type u_1} [LE α] (s : ) (t : ) :
(s t).compl = s.compl t.compl
@[simp]
theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s : ) (t : ) :
(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 ()) :
(sSup S).compl = sS, s.compl
@[simp]
theorem UpperSet.compl_sInf {α : Type u_1} [LE α] (S : Set ()) :
(sInf S).compl = sS, s.compl
@[simp]
theorem UpperSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
@[simp]
theorem UpperSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
theorem UpperSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [LE α] (f : (i : ι) → κ i) :
(⨆ (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 : ι) → κ i) :
(⨅ (i : ι), ⨅ (j : κ i), f i j).compl = ⨅ (i : ι), ⨅ (j : κ i), (f i j).compl
@[simp]
theorem LowerSet.coe_compl {α : Type u_1} [LE α] (s : ) :
s.compl = (s)
@[simp]
theorem LowerSet.mem_compl_iff {α : Type u_1} [LE α] {s : } {a : α} :
a s.compl as
@[simp]
theorem LowerSet.compl_compl {α : Type u_1} [LE α] (s : ) :
s.compl.compl = s
@[simp]
theorem LowerSet.compl_le_compl {α : Type u_1} [LE α] {s : } {t : } :
s.compl t.compl s t
theorem LowerSet.compl_sup {α : Type u_1} [LE α] (s : ) (t : ) :
(s t).compl = s.compl t.compl
theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s : ) (t : ) :
(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 ()) :
(sSup S).compl = sS, s.compl
theorem LowerSet.compl_sInf {α : Type u_1} [LE α] (S : Set ()) :
(sInf S).compl = sS, s.compl
theorem LowerSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
theorem LowerSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
(⨅ (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 : ι) → κ i) :
(⨆ (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 : ι) → κ i) :
(⨅ (i : ι), ⨅ (j : κ i), f i j).compl = ⨅ (i : ι), ⨅ (j : κ i), (f i j).compl
@[simp]
theorem upperSetIsoLowerSet_symm_apply {α : Type u_1} [LE α] (s : ) :
(RelIso.symm upperSetIsoLowerSet) s = s.compl
@[simp]
theorem upperSetIsoLowerSet_apply {α : Type u_1} [LE α] (s : ) :
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} [] :
IsTotal () fun (x x_1 : ) => x x_1
Equations
• =
instance LowerSet.isTotal_le {α : Type u_1} [] :
IsTotal () fun (x x_1 : ) => x x_1
Equations
• =
noncomputable instance instCompleteLinearOrderUpperSet {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance instCompleteLinearOrderLowerSet {α : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.

#### Map #

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

#### Principal sets #

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

The smallest upper set containing a given element.

Equations
• = { carrier := , upper' := }
Instances For
def UpperSet.Ioi {α : Type u_1} [] (a : α) :

The smallest upper set containing a given element.

Equations
• = { carrier := , upper' := }
Instances For
@[simp]
theorem UpperSet.coe_Ici {α : Type u_1} [] (a : α) :
() =
@[simp]
theorem UpperSet.coe_Ioi {α : Type u_1} [] (a : α) :
() =
@[simp]
theorem UpperSet.mem_Ici_iff {α : Type u_1} [] {a : α} {b : α} :
a b
@[simp]
theorem UpperSet.mem_Ioi_iff {α : Type u_1} [] {a : α} {b : α} :
a < b
@[simp]
theorem UpperSet.map_Ici {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) (a : α) :
() () = UpperSet.Ici (f a)
@[simp]
theorem UpperSet.map_Ioi {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) (a : α) :
() () = UpperSet.Ioi (f a)
theorem UpperSet.Ici_le_Ioi {α : Type u_1} [] (a : α) :
@[simp]
theorem UpperSet.Ici_bot {α : Type u_1} [] [] :
@[simp]
theorem UpperSet.Ioi_top {α : Type u_1} [] [] :
@[simp]
theorem UpperSet.Ici_ne_top {α : Type u_1} [] {a : α} :
@[simp]
theorem UpperSet.Ici_lt_top {α : Type u_1} [] {a : α} :
@[simp]
theorem UpperSet.le_Ici {α : Type u_1} [] {s : } {a : α} :
a s
theorem UpperSet.Ici_injective {α : Type u_1} [] :
Function.Injective UpperSet.Ici
@[simp]
theorem UpperSet.Ici_inj {α : Type u_1} [] {a : α} {b : α} :
a = b
theorem UpperSet.Ici_ne_Ici {α : Type u_1} [] {a : α} {b : α} :
a b
@[simp]
theorem UpperSet.Ici_sup {α : Type u_1} [] (a : α) (b : α) :
@[simp]
theorem UpperSet.Ici_sSup {α : Type u_1} [] (S : Set α) :
UpperSet.Ici (sSup S) = aS,
@[simp]
theorem UpperSet.Ici_iSup {α : Type u_1} {ι : Sort u_4} [] (f : ια) :
UpperSet.Ici (⨆ (i : ι), f i) = ⨆ (i : ι), UpperSet.Ici (f i)
theorem UpperSet.Ici_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [] (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} [] (a : α) :

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

Equations
• = { carrier := , lower' := }
Instances For
def LowerSet.Iio {α : Type u_1} [] (a : α) :

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

Equations
• = { carrier := , lower' := }
Instances For
@[simp]
theorem LowerSet.coe_Iic {α : Type u_1} [] (a : α) :
() =
@[simp]
theorem LowerSet.coe_Iio {α : Type u_1} [] (a : α) :
() =
@[simp]
theorem LowerSet.mem_Iic_iff {α : Type u_1} [] {a : α} {b : α} :
b a
@[simp]
theorem LowerSet.mem_Iio_iff {α : Type u_1} [] {a : α} {b : α} :
b < a
@[simp]
theorem LowerSet.map_Iic {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) (a : α) :
() () = LowerSet.Iic (f a)
@[simp]
theorem LowerSet.map_Iio {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) (a : α) :
() () = LowerSet.Iio (f a)
theorem LowerSet.Ioi_le_Ici {α : Type u_1} [] (a : α) :
@[simp]
theorem LowerSet.Iic_top {α : Type u_1} [] [] :
@[simp]
theorem LowerSet.Iio_bot {α : Type u_1} [] [] :
@[simp]
theorem LowerSet.Iic_ne_bot {α : Type u_1} [] {a : α} :
@[simp]
theorem LowerSet.bot_lt_Iic {α : Type u_1} [] {a : α} :
@[simp]
theorem LowerSet.Iic_le {α : Type u_1} [] {s : } {a : α} :
a s
theorem LowerSet.Iic_injective {α : Type u_1} [] :
Function.Injective LowerSet.Iic
@[simp]
theorem LowerSet.Iic_inj {α : Type u_1} [] {a : α} {b : α} :
a = b
theorem LowerSet.Iic_ne_Iic {α : Type u_1} [] {a : α} {b : α} :
a b
@[simp]
theorem LowerSet.Iic_inf {α : Type u_1} [] (a : α) (b : α) :
@[simp]
theorem LowerSet.Iic_sInf {α : Type u_1} [] (S : Set α) :
LowerSet.Iic (sInf S) = aS,
@[simp]
theorem LowerSet.Iic_iInf {α : Type u_1} {ι : Sort u_4} [] (f : ια) :
LowerSet.Iic (⨅ (i : ι), f i) = ⨅ (i : ι), LowerSet.Iic (f i)
theorem LowerSet.Iic_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_5} [] (f : (i : ι) → κ iα) :
LowerSet.Iic (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), LowerSet.Iic (f i j)
def upperClosure {α : Type u_1} [] (s : Set α) :

The greatest upper set containing a given set.

Equations
• = { carrier := {x : α | as, a x}, upper' := }
Instances For
def lowerClosure {α : Type u_1} [] (s : Set α) :

The least lower set containing a given set.

Equations
• = { carrier := {x : α | as, x a}, lower' := }
Instances For
@[simp]
theorem mem_upperClosure {α : Type u_1} [] {s : Set α} {x : α} :
as, a x
@[simp]
theorem mem_lowerClosure {α : Type u_1} [] {s : Set α} {x : α} :
as, x a
theorem coe_upperClosure {α : Type u_1} [] (s : Set α) :
() = as,
theorem coe_lowerClosure {α : Type u_1} [] (s : Set α) :
() = as,
instance instDecidablePredMemUpperClosure {α : Type u_1} [] {s : Set α} [DecidablePred fun (x : α) => as, a x] :
DecidablePred fun (x : α) =>
Equations
• instDecidablePredMemUpperClosure = inst
instance instDecidablePredMemLowerClosure {α : Type u_1} [] {s : Set α} [DecidablePred fun (x : α) => as, x a] :
DecidablePred fun (x : α) =>
Equations
• instDecidablePredMemLowerClosure = inst
theorem subset_upperClosure {α : Type u_1} [] {s : Set α} :
s ()
theorem subset_lowerClosure {α : Type u_1} [] {s : Set α} :
s ()
theorem upperClosure_min {α : Type u_1} [] {s : Set α} {t : Set α} (h : s t) (ht : ) :
() t
theorem lowerClosure_min {α : Type u_1} [] {s : Set α} {t : Set α} (h : s t) (ht : ) :
() t
theorem IsUpperSet.upperClosure {α : Type u_1} [] {s : Set α} (hs : ) :
() = s
theorem IsLowerSet.lowerClosure {α : Type u_1} [] {s : Set α} (hs : ) :
() = s
@[simp]
theorem UpperSet.upperClosure {α : Type u_1} [] (s : ) :
= s
@[simp]
theorem LowerSet.lowerClosure {α : Type u_1} [] (s : ) :
= s
@[simp]
theorem upperClosure_image {α : Type u_1} {β : Type u_2} [] [] {s : Set α} (f : α ≃o β) :
upperClosure (f '' s) = () ()
@[simp]
theorem lowerClosure_image {α : Type u_1} {β : Type u_2} [] [] {s : Set α} (f : α ≃o β) :
lowerClosure (f '' s) = () ()
@[simp]
theorem UpperSet.iInf_Ici {α : Type u_1} [] (s : Set α) :
as, =
@[simp]
theorem LowerSet.iSup_Iic {α : Type u_1} [] (s : Set α) :
as, =
@[simp]
theorem lowerClosure_le {α : Type u_1} [] {s : Set α} {t : } :
s t
@[simp]
theorem le_upperClosure {α : Type u_1} [] {t : Set α} {s : } :
t s
theorem gc_upperClosure_coe {α : Type u_1} [] :
GaloisConnection (OrderDual.toDual upperClosure) (SetLike.coe OrderDual.ofDual)
theorem gc_lowerClosure_coe {α : Type u_1} [] :
GaloisConnection lowerClosure SetLike.coe
def giUpperClosureCoe {α : Type u_1} [] :
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} [] :
GaloisInsertion lowerClosure SetLike.coe

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

Equations
• giLowerClosureCoe = { choice := fun (s : Set α) (hs : () s) => { carrier := s, lower' := }, gc := , le_l_u := , choice_eq := }
Instances For
theorem upperClosure_anti {α : Type u_1} [] :
Antitone upperClosure
theorem lowerClosure_mono {α : Type u_1} [] :
Monotone lowerClosure
@[simp]
theorem upperClosure_empty {α : Type u_1} [] :
@[simp]
theorem lowerClosure_empty {α : Type u_1} [] :
@[simp]
theorem upperClosure_singleton {α : Type u_1} [] (a : α) :
@[simp]
theorem lowerClosure_singleton {α : Type u_1} [] (a : α) :
@[simp]
theorem upperClosure_univ {α : Type u_1} [] :
upperClosure Set.univ =
@[simp]
theorem lowerClosure_univ {α : Type u_1} [] :
lowerClosure Set.univ =
@[simp]
theorem upperClosure_eq_top_iff {α : Type u_1} [] {s : Set α} :
s =
@[simp]
theorem lowerClosure_eq_bot_iff {α : Type u_1} [] {s : Set α} :
s =
@[simp]
theorem upperClosure_union {α : Type u_1} [] (s : Set α) (t : Set α) :
@[simp]
theorem lowerClosure_union {α : Type u_1} [] (s : Set α) (t : Set α) :
@[simp]
theorem upperClosure_iUnion {α : Type u_1} {ι : Sort u_4} [] (f : ιSet α) :
upperClosure (⋃ (i : ι), f i) = ⨅ (i : ι), upperClosure (f i)
@[simp]
theorem lowerClosure_iUnion {α : Type u_1} {ι : Sort u_4} [] (f : ιSet α) :
lowerClosure (⋃ (i : ι), f i) = ⨆ (i : ι), lowerClosure (f i)
@[simp]
theorem upperClosure_sUnion {α : Type u_1} [] (S : Set (Set α)) :
upperClosure (⋃₀ S) = sS,
@[simp]
theorem lowerClosure_sUnion {α : Type u_1} [] (S : Set (Set α)) :
lowerClosure (⋃₀ S) = sS,
theorem Set.OrdConnected.upperClosure_inter_lowerClosure {α : Type u_1} [] {s : Set α} (h : s.OrdConnected) :
() () = s
theorem ordConnected_iff_upperClosure_inter_lowerClosure {α : Type u_1} [] {s : Set α} :
s.OrdConnected () () = s
@[simp]
theorem upperBounds_lowerClosure {α : Type u_1} [] {s : Set α} :
@[simp]
theorem lowerBounds_upperClosure {α : Type u_1} [] {s : Set α} :
@[simp]
theorem bddAbove_lowerClosure {α : Type u_1} [] {s : Set α} :
BddAbove ()
@[simp]
theorem bddBelow_upperClosure {α : Type u_1} [] {s : Set α} :
BddBelow ()
theorem BddAbove.lowerClosure {α : Type u_1} [] {s : Set α} :
BddAbove ()

Alias of the reverse direction of bddAbove_lowerClosure.

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

Alias of the forward direction of bddAbove_lowerClosure.

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

Alias of the forward direction of bddBelow_upperClosure.

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

Alias of the reverse direction of bddBelow_upperClosure.

@[simp]
theorem IsLowerSet.disjoint_upperClosure_left {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
Disjoint (()) t Disjoint s t
@[simp]
theorem IsLowerSet.disjoint_upperClosure_right {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) :
Disjoint s () Disjoint s t
@[simp]
theorem IsUpperSet.disjoint_lowerClosure_left {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
Disjoint (()) t Disjoint s t
@[simp]
theorem IsUpperSet.disjoint_lowerClosure_right {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) :
Disjoint s () Disjoint s t

### Set Difference #

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

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

Equations
• s.sdiff t = { carrier := s \ (), lower' := }
Instances For
def LowerSet.erase {α : Type u_1} [] (s : ) (a : α) :

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

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

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

Equations
• s.sdiff t = { carrier := s \ (), upper' := }
Instances For
def UpperSet.erase {α : Type u_1} [] (s : ) (a : α) :

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

Equations
• s.erase a = { carrier := s \ (), upper' := }
Instances For
@[simp]
theorem UpperSet.coe_sdiff {α : Type u_1} [] (s : ) (t : Set α) :
(s.sdiff t) = s \ ()
@[simp]
theorem UpperSet.coe_erase {α : Type u_1} [] (s : ) (a : α) :
(s.erase a) = s \ ()
@[simp]
theorem UpperSet.sdiff_singleton {α : Type u_1} [] (s : ) (a : α) :
s.sdiff {a} = s.erase a
theorem UpperSet.le_sdiff_left {α : Type u_1} [] {s : } {t : Set α} :
s s.sdiff t
theorem UpperSet.le_erase {α : Type u_1} [] {s : } {a : α} :
s s.erase a
@[simp]
theorem UpperSet.sdiff_eq_left {α : Type u_1} [] {s : } {t : Set α} :
s.sdiff t = s Disjoint (s) t
@[simp]
theorem UpperSet.erase_eq {α : Type u_1} [] {s : } {a : α} :
s.erase a = s as
@[simp]
theorem UpperSet.lt_sdiff_left {α : Type u_1} [] {s : } {t : Set α} :
s < s.sdiff t ¬Disjoint (s) t
@[simp]
theorem UpperSet.lt_erase {α : Type u_1} [] {s : } {a : α} :
s < s.erase a a s
@[simp]
theorem UpperSet.sdiff_idem {α : Type u_1} [] (s : ) (t : Set α) :
(s.sdiff t).sdiff t = s.sdiff t
@[simp]
theorem UpperSet.erase_idem {α : Type u_1} [] (s : ) (a : α) :
(s.erase a).erase a = s.erase a
theorem UpperSet.sdiff_inf_upperClosure {α : Type u_1} [] {s : } {t : Set α} (hts : t s) (hst : bs, ct, b cb t) :
s.sdiff t = s
theorem UpperSet.upperClosure_inf_sdiff {α : Type u_1} [] {s : } {t : Set α} (hts : t s) (hst : bs, ct, b cb t) :
s.sdiff t = s
theorem UpperSet.erase_inf_Ici {α : Type u_1} [] {s : } {a : α} (ha : a s) (has : bs, b ab = a) :
s.erase a = s
theorem UpperSet.Ici_inf_erase {α : Type u_1} [] {s : } {a : α} (ha : a s) (has : bs, b ab = a) :
s.erase a = s

### Product #

theorem IsUpperSet.prod {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem IsLowerSet.prod {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
def UpperSet.prod {α : Type u_1} {β : Type u_2} [] [] (s : ) (t : ) :
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} [] [] :
SProd () () (UpperSet (α × β))
Equations
• UpperSet.instSProd = { sprod := UpperSet.prod }
@[simp]
theorem UpperSet.coe_prod {α : Type u_1} {β : Type u_2} [] [] (s : ) (t : ) :
(s ×ˢ t) = s ×ˢ t
@[simp]
theorem UpperSet.mem_prod {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {s : } {t : } :
x s ×ˢ t x.1 s x.2 t
theorem UpperSet.Ici_prod {α : Type u_1} {β : Type u_2} [] [] (x : α × β) :
@[simp]
theorem UpperSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [] [] (a : α) (b : β) :
= UpperSet.Ici (a, b)
@[simp]
theorem UpperSet.prod_top {α : Type u_1} {β : Type u_2} [] [] (s : ) :
@[simp]
theorem UpperSet.top_prod {α : Type u_1} {β : Type u_2} [] [] (t : ) :
@[simp]
theorem UpperSet.bot_prod_bot {α : Type u_1} {β : Type u_2} [] [] :
@[simp]
theorem UpperSet.sup_prod {α : Type u_1} {β : Type u_2} [] [] (s₁ : ) (s₂ : ) (t : ) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem UpperSet.prod_sup {α : Type u_1} {β : Type u_2} [] [] (s : ) (t₁ : ) (t₂ : ) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem UpperSet.inf_prod {α : Type u_1} {β : Type u_2} [] [] (s₁ : ) (s₂ : ) (t : ) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem UpperSet.prod_inf {α : Type u_1} {β : Type u_2} [] [] (s : ) (t₁ : ) (t₂ : ) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
theorem UpperSet.prod_sup_prod {α : Type u_1} {β : Type u_2} [] [] (s₁ : ) (s₂ : ) (t₁ : ) (t₂ : ) :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
theorem UpperSet.prod_mono {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ ×ˢ t₁ s₂ ×ˢ t₂
theorem UpperSet.prod_mono_left {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ ×ˢ t s₂ ×ˢ t
theorem UpperSet.prod_mono_right {α : Type u_1} {β : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
t₁ t₂s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem UpperSet.prod_self_le_prod_self {α : Type u_1} [] {s₁ : } {s₂ : } :
s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
@[simp]
theorem UpperSet.prod_self_lt_prod_self {α : Type u_1} [] {s₁ : } {s₂ : } :
s₁ ×ˢ s₁ < s₂ ×ˢ s₂ s₁ < s₂
theorem UpperSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ s₁ s₂ t₁ t₂ s₂ = t₂ =
@[simp]
theorem UpperSet.prod_eq_top {α : Type u_1} {β : Type u_2} [] [] {s : } {t : } :
s ×ˢ t = s = t =
@[simp]
theorem UpperSet.codisjoint_prod {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) Codisjoint s₁ s₂ Codisjoint t₁ t₂
def LowerSet.prod {α : Type u_1} {β : Type u_2} [] [] (s : ) (t : ) :
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} [] [] :
SProd () () (LowerSet (α × β))
Equations
• LowerSet.instSProd = { sprod := LowerSet.prod }
@[simp]
theorem LowerSet.coe_prod {α : Type u_1} {β : Type u_2} [] [] (s : ) (t : ) :
(s ×ˢ t) = s ×ˢ t
@[simp]
theorem LowerSet.mem_prod {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {s : } {t : } :
x s ×ˢ t x.1 s x.2 t
theorem LowerSet.Iic_prod {α : Type u_1} {β : Type u_2} [] [] (x : α × β) :
@[simp]
theorem LowerSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [] [] (a : α) (b : β) :
= LowerSet.Iic (a, b)
@[simp]
theorem LowerSet.prod_bot {α : Type u_1} {β : Type u_2} [] [] (s : ) :
@[simp]
theorem LowerSet.bot_prod {α : Type u_1} {β : Type u_2} [] [] (t : ) :
@[simp]
theorem LowerSet.top_prod_top {α : Type u_1} {β : Type u_2} [] [] :
@[simp]
theorem LowerSet.inf_prod {α : Type u_1} {β : Type u_2} [] [] (s₁ : ) (s₂ : ) (t : ) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem LowerSet.prod_inf {α : Type u_1} {β : Type u_2} [] [] (s : ) (t₁ : ) (t₂ : ) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem LowerSet.sup_prod {α : Type u_1} {β : Type u_2} [] [] (s₁ : ) (s₂ : ) (t : ) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem LowerSet.prod_sup {α : Type u_1} {β : Type u_2} [] [] (s : ) (t₁ : ) (t₂ : ) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
theorem LowerSet.prod_inf_prod {α : Type u_1} {β : Type u_2} [] [] (s₁ : ) (s₂ : ) (t₁ : ) (t₂ : ) :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
theorem LowerSet.prod_mono {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ s₂t₁ t₂s₁ ×ˢ t₁ s₂ ×ˢ t₂
theorem LowerSet.prod_mono_left {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t : } :
s₁ s₂s₁ ×ˢ t s₂ ×ˢ t
theorem LowerSet.prod_mono_right {α : Type u_1} {β : Type u_2} [] [] {s : } {t₁ : } {t₂ : } :
t₁ t₂s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem LowerSet.prod_self_le_prod_self {α : Type u_1} [] {s₁ : } {s₂ : } :
s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
@[simp]
theorem LowerSet.prod_self_lt_prod_self {α : Type u_1} [] {s₁ : } {s₂ : } :
s₁ ×ˢ s₁ < s₂ ×ˢ s₂ s₁ < s₂
theorem LowerSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ s₁ s₂ t₁ t₂ s₁ = t₁ =
@[simp]
theorem LowerSet.prod_eq_bot {α : Type u_1} {β : Type u_2} [] [] {s : } {t : } :
s ×ˢ t = s = t =
@[simp]
theorem LowerSet.disjoint_prod {α : Type u_1} {β : Type u_2} [] [] {s₁ : } {s₂ : } {t₁ : } {t₂ : } :
Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) Disjoint s₁ s₂ Disjoint t₁ t₂
@[simp]
theorem upperClosure_prod {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (t : Set β) :
@[simp]
theorem lowerClosure_prod {α : Type u_1} {β : Type u_2} [] [] (s : Set α) (t : Set β) :