# 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 : ) :
theorem IsLowerSet.ordConnected {α : Type u_1} [] {s : Set α} (h : ) :
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
theorem IsLowerSet.lowerBounds_subset {α : Type u_1} [] {s : Set α} (hs : ) :
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 : ) :
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 : ) :
theorem IsLowerSet.not_bot_mem {α : Type u_1} [] {s : Set α} [] (hs : ) :
s s =
theorem IsUpperSet.not_bddAbove {α : Type u_1} [] {s : Set α} [] (hs : ) :
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 : ) :
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
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
instance UpperSet.instSetLikeUpperSet {α : Type u_1} [LE α] :
SetLike () α
Equations
• UpperSet.instSetLikeUpperSet = { coe := UpperSet.carrier, coe_injective' := (_ : ∀ (s t : ), s.carrier = t.carriers = t) }
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.instSetLikeLowerSet {α : Type u_1} [LE α] :
SetLike () α
Equations
• LowerSet.instSetLikeLowerSet = { coe := LowerSet.carrier, coe_injective' := (_ : ∀ (s t : ), s.carrier = t.carriers = t) }
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.instSupUpperSet {α : Type u_1} [LE α] :
Sup ()
Equations
• UpperSet.instSupUpperSet = { sup := fun (s t : ) => { carrier := s t, upper' := (_ : IsUpperSet (s t)) } }
instance UpperSet.instInfUpperSet {α : Type u_1} [LE α] :
Inf ()
Equations
• UpperSet.instInfUpperSet = { inf := fun (s t : ) => { carrier := s t, upper' := (_ : IsUpperSet (s t)) } }
instance UpperSet.instTopUpperSet {α : Type u_1} [LE α] :
Top ()
Equations
• UpperSet.instTopUpperSet = { top := { carrier := , upper' := (_ : ) } }
instance UpperSet.instBotUpperSet {α : Type u_1} [LE α] :
Bot ()
Equations
• UpperSet.instBotUpperSet = { bot := { carrier := Set.univ, upper' := (_ : IsUpperSet Set.univ) } }
instance UpperSet.instSupSetUpperSet {α : Type u_1} [LE α] :
Equations
• UpperSet.instSupSetUpperSet = { sSup := fun (S : Set ()) => { carrier := ⋂ s ∈ S, s, upper' := (_ : IsUpperSet (⋂ i ∈ S, i)) } }
instance UpperSet.instInfSetUpperSet {α : Type u_1} [LE α] :
Equations
• UpperSet.instInfSetUpperSet = { sInf := fun (S : Set ()) => { carrier := ⋃ s ∈ S, s, upper' := (_ : IsUpperSet (⋃ i ∈ S, i)) } }
instance UpperSet.completelyDistribLattice {α : Type u_1} [LE α] :
Equations
• One or more equations did not get rendered due to their size.
instance UpperSet.instInhabitedUpperSet {α : Type u_1} [LE α] :
Equations
• UpperSet.instInhabitedUpperSet = { 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 : } :
@[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) = ⋂ s ∈ S, s
@[simp]
theorem UpperSet.coe_sInf {α : Type u_1} [LE α] (S : Set ()) :
(sInf S) = ⋃ s ∈ S, 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 ∃ s ∈ S, 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.instSupLowerSet {α : Type u_1} [LE α] :
Sup ()
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 α] :
Inf ()
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 α] :
Top ()
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 α] :
Bot ()
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 : Set ()) => { carrier := ⋃ s ∈ S, s, lower' := (_ : IsLowerSet (⋃ i ∈ S, i)) } }
instance LowerSet.instInfSetLowerSet {α : Type u_1} [LE α] :
Equations
• LowerSet.instInfSetLowerSet = { sInf := fun (S : Set ()) => { carrier := ⋂ s ∈ S, s, lower' := (_ : IsLowerSet (⋂ i ∈ S, i)) } }
instance LowerSet.completelyDistribLattice {α : Type u_1} [LE α] :
Equations
• One or more equations did not get rendered due to their size.
instance LowerSet.instInhabitedLowerSet {α : Type u_1} [LE α] :
Equations
• LowerSet.instInhabitedLowerSet = { 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 : } :
@[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) = ⋃ s ∈ S, s
@[simp]
theorem LowerSet.coe_sInf {α : Type u_1} [LE α] (S : Set ()) :
(sInf S) = ⋂ s ∈ S, 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 ∃ s ∈ S, 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
Instances For
def LowerSet.compl {α : Type u_1} [LE α] (s : ) :

The complement of a lower set as an upper set.

Equations
Instances For
@[simp]
theorem UpperSet.coe_compl {α : Type u_1} [LE α] (s : ) :
() = (s)
@[simp]
theorem UpperSet.mem_compl_iff {α : Type u_1} [LE α] {s : } {a : α} :
as
@[simp]
theorem UpperSet.compl_compl {α : Type u_1} [LE α] (s : ) :
@[simp]
theorem UpperSet.compl_le_compl {α : Type u_1} [LE α] {s : } {t : } :
s t
@[simp]
theorem UpperSet.compl_sup {α : Type u_1} [LE α] (s : ) (t : ) :
@[simp]
theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s : ) (t : ) :
@[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 ()) :
= ⨆ s ∈ S,
@[simp]
theorem UpperSet.compl_sInf {α : Type u_1} [LE α] (S : Set ()) :
= ⨅ s ∈ S,
@[simp]
theorem UpperSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
UpperSet.compl (⨆ (i : ι), f i) = ⨆ (i : ι), UpperSet.compl (f i)
@[simp]
theorem UpperSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
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 : ι) → κ i) :
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 : ι) → κ i) :
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 : ) :
() = (s)
@[simp]
theorem LowerSet.mem_compl_iff {α : Type u_1} [LE α] {s : } {a : α} :
as
@[simp]
theorem LowerSet.compl_compl {α : Type u_1} [LE α] (s : ) :
@[simp]
theorem LowerSet.compl_le_compl {α : Type u_1} [LE α] {s : } {t : } :
s t
theorem LowerSet.compl_sup {α : Type u_1} [LE α] (s : ) (t : ) :
theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s : ) (t : ) :
theorem LowerSet.compl_top {α : Type u_1} [LE α] :
theorem LowerSet.compl_bot {α : Type u_1} [LE α] :
theorem LowerSet.compl_sSup {α : Type u_1} [LE α] (S : Set ()) :
= ⨆ s ∈ S,
theorem LowerSet.compl_sInf {α : Type u_1} [LE α] (S : Set ()) :
= ⨅ s ∈ S,
theorem LowerSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
LowerSet.compl (⨆ (i : ι), f i) = ⨆ (i : ι), LowerSet.compl (f i)
theorem LowerSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι) :
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 : ι) → κ i) :
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 : ι) → κ i) :
LowerSet.compl (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), LowerSet.compl (f i j)
@[simp]
theorem upperSetIsoLowerSet_symm_apply {α : Type u_1} [LE α] (s : ) :
(RelIso.symm upperSetIsoLowerSet) s =
@[simp]
theorem upperSetIsoLowerSet_apply {α : Type u_1} [LE α] (s : ) :
upperSetIsoLowerSet 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
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
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} [] [] (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 β) :
@[simp]
theorem UpperSet.mem_map {α : Type u_1} {β : Type u_2} [] [] {f : α ≃o β} {s : } {b : β} :
b () s () 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) = () 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 β) :
@[simp]
theorem LowerSet.mem_map {α : Type u_1} {β : Type u_2} [] [] {s : } {f : α ≃o β} {b : β} :
b () s () 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) = () 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 : ) :
UpperSet.compl (() s) = () ()
@[simp]
theorem LowerSet.compl_map {α : Type u_1} {β : Type u_2} [] [] (f : α ≃o β) (s : ) :
LowerSet.compl (() s) = () ()

#### 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) = ⨆ a ∈ S,
@[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) = ⨅ a ∈ S,
@[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 : α | ∃ a ∈ s, a x}, upper' := (_ : ∀ (x x_1 : α), x x_1x {x : α | ∃ a ∈ s, a x}∃ a ∈ s, a x_1) }
Instances For
def lowerClosure {α : Type u_1} [] (s : Set α) :

The least lower set containing a given set.

Equations
• = { carrier := {x : α | ∃ a ∈ s, x a}, lower' := (_ : ∀ (x x_1 : α), x_1 xx {x : α | ∃ a ∈ s, x a}∃ a ∈ s, x_1 a) }
Instances For
@[simp]
theorem mem_upperClosure {α : Type u_1} [] {s : Set α} {x : α} :
∃ a ∈ s, a x
@[simp]
theorem mem_lowerClosure {α : Type u_1} [] {s : Set α} {x : α} :
∃ a ∈ s, x a
theorem coe_upperClosure {α : Type u_1} [] (s : Set α) :
() = ⋃ a ∈ s,
theorem coe_lowerClosure {α : Type u_1} [] (s : Set α) :
() = ⋃ a ∈ s,
instance instDecidablePredMemUpperClosure {α : Type u_1} [] {s : Set α} [DecidablePred fun (x : α) => ∃ a ∈ s, a x] :
DecidablePred fun (x : α) =>
Equations
• instDecidablePredMemUpperClosure = inst
instance instDecidablePredMemLowerClosure {α : Type u_1} [] {s : Set α} [DecidablePred fun (x : α) => ∃ a ∈ s, 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 α) :
⨅ a ∈ s, =
@[simp]
theorem LowerSet.iSup_Iic {α : Type u_1} [] (s : Set α) :
⨆ a ∈ s, =
@[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
• One or more equations did not get rendered due to their size.
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) = ⨅ s ∈ S,
@[simp]
theorem lowerClosure_sUnion {α : Type u_1} [] (S : Set (Set α)) :
lowerClosure (⋃₀ S) = ⨆ s ∈ S,
theorem Set.OrdConnected.upperClosure_inter_lowerClosure {α : Type u_1} [] {s : Set α} (h : ) :
() () = s
theorem ordConnected_iff_upperClosure_inter_lowerClosure {α : Type u_1} [] {s : Set α} :
() () = 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.of_lowerClosure {α : Type u_1} [] {s : Set α} :
BddAbove ()

Alias of the forward direction of bddAbove_lowerClosure.

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

Alias of the reverse 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
• = { carrier := s \ (), lower' := (_ : IsLowerSet (s \ ())) }
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
• = { carrier := s \ (), lower' := (_ : IsLowerSet (s \ ())) }
Instances For
@[simp]
theorem LowerSet.coe_sdiff {α : Type u_1} [] (s : ) (t : Set α) :
() = s \ ()
@[simp]
theorem LowerSet.coe_erase {α : Type u_1} [] (s : ) (a : α) :
() = s \ ()
@[simp]
theorem LowerSet.sdiff_singleton {α : Type u_1} [] (s : ) (a : α) :
theorem LowerSet.sdiff_le_left {α : Type u_1} [] {s : } {t : Set α} :
s
theorem LowerSet.erase_le {α : Type u_1} [] {s : } {a : α} :
s
@[simp]
theorem LowerSet.sdiff_eq_left {α : Type u_1} [] {s : } {t : Set α} :
= s Disjoint (s) t
@[simp]
theorem LowerSet.erase_eq {α : Type u_1} [] {s : } {a : α} :
= s as
@[simp]
theorem LowerSet.sdiff_lt_left {α : Type u_1} [] {s : } {t : Set α} :
< s ¬Disjoint (s) t
@[simp]
theorem LowerSet.erase_lt {α : Type u_1} [] {s : } {a : α} :
< s a s
@[simp]
theorem LowerSet.sdiff_idem {α : Type u_1} [] (s : ) (t : Set α) :
@[simp]
theorem LowerSet.erase_idem {α : Type u_1} [] (s : ) (a : α) :
theorem LowerSet.sdiff_sup_lowerClosure {α : Type u_1} [] {s : } {t : Set α} (hts : t s) (hst : bs, ct, c bb t) :
= s
theorem LowerSet.lowerClosure_sup_sdiff {α : Type u_1} [] {s : } {t : Set α} (hts : t s) (hst : bs, ct, c bb t) :
= s
theorem LowerSet.erase_sup_Iic {α : Type u_1} [] {s : } {a : α} (ha : a s) (has : bs, a bb = a) :
= s
theorem LowerSet.Iic_sup_erase {α : Type u_1} [] {s : } {a : α} (ha : a s) (has : bs, a bb = 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
• = { carrier := s \ (), upper' := (_ : IsUpperSet (s \ ())) }
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
• = { carrier := s \ (), upper' := (_ : IsUpperSet (s \ ())) }
Instances For
@[simp]
theorem UpperSet.coe_sdiff {α : Type u_1} [] (s : ) (t : Set α) :
() = s \ ()
@[simp]
theorem UpperSet.coe_erase {α : Type u_1} [] (s : ) (a : α) :
() = s \ ()
@[simp]
theorem UpperSet.sdiff_singleton {α : Type u_1} [] (s : ) (a : α) :
theorem UpperSet.le_sdiff_left {α : Type u_1} [] {s : } {t : Set α} :
s
theorem UpperSet.le_erase {α : Type u_1} [] {s : } {a : α} :
s
@[simp]
theorem UpperSet.sdiff_eq_left {α : Type u_1} [] {s : } {t : Set α} :
= s Disjoint (s) t
@[simp]
theorem UpperSet.erase_eq {α : Type u_1} [] {s : } {a : α} :
= s as
@[simp]
theorem UpperSet.lt_sdiff_left {α : Type u_1} [] {s : } {t : Set α} :
s < ¬Disjoint (s) t
@[simp]
theorem UpperSet.lt_erase {α : Type u_1} [] {s : } {a : α} :
s < a s
@[simp]
theorem UpperSet.sdiff_idem {α : Type u_1} [] (s : ) (t : Set α) :
@[simp]
theorem UpperSet.erase_idem {α : Type u_1} [] (s : ) (a : α) :
theorem UpperSet.sdiff_inf_upperClosure {α : Type u_1} [] {s : } {t : Set α} (hts : t s) (hst : bs, ct, b cb t) :
= s
theorem UpperSet.upperClosure_inf_sdiff {α : Type u_1} [] {s : } {t : Set α} (hts : t s) (hst : bs, ct, b cb t) :
= s
theorem UpperSet.erase_inf_Ici {α : Type u_1} [] {s : } {a : α} (ha : a s) (has : bs, b ab = a) :
= s
theorem UpperSet.Ici_inf_erase {α : Type u_1} [] {s : } {a : α} (ha : a s) (has : bs, b ab = 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
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
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 β) :