# mathlib3documentation

order.upper_lower.basic

# Up-sets and down-sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines upper and lower sets in an order.

## Main declarations #

• `is_upper_set`: 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.
• `is_lower_set`: 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.
• `upper_set`: The type of upper sets.
• `lower_set`: The type of lower sets.
• `upper_closure`: The greatest upper set containing a set.
• `lower_closure`: The least lower set containing a set.
• `upper_set.Ici`: Principal upper set. `set.Ici` as an upper set.
• `upper_set.Ioi`: Strict principal upper set. `set.Ioi` as an upper set.
• `lower_set.Iic`: Principal lower set. `set.Iic` as an lower set.
• `lower_set.Iio`: Strict principal lower set. `set.Iio` as an lower set.

## Notation #

`×ˢ` is notation for `upper_set.prod`/`lower_set.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 is_upper_set {α : Type u_1} [has_le α] (s : set α) :
Prop

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
def is_lower_set {α : Type u_1} [has_le α] (s : set α) :
Prop

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
theorem is_upper_set_empty {α : Type u_1} [has_le α] :
theorem is_lower_set_empty {α : Type u_1} [has_le α] :
theorem is_upper_set_univ {α : Type u_1} [has_le α] :
theorem is_lower_set_univ {α : Type u_1} [has_le α] :
theorem is_upper_set.compl {α : Type u_1} [has_le α] {s : set α} (hs : is_upper_set s) :
theorem is_lower_set.compl {α : Type u_1} [has_le α] {s : set α} (hs : is_lower_set s) :
@[simp]
theorem is_upper_set_compl {α : Type u_1} [has_le α] {s : set α} :
@[simp]
theorem is_lower_set_compl {α : Type u_1} [has_le α] {s : set α} :
theorem is_upper_set.union {α : Type u_1} [has_le α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
theorem is_lower_set.union {α : Type u_1} [has_le α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
theorem is_upper_set.inter {α : Type u_1} [has_le α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
theorem is_lower_set.inter {α : Type u_1} [has_le α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
theorem is_upper_set_Union {α : Type u_1} {ι : Sort u_4} [has_le α] {f : ι set α} (hf : (i : ι), is_upper_set (f i)) :
is_upper_set ( (i : ι), f i)
theorem is_lower_set_Union {α : Type u_1} {ι : Sort u_4} [has_le α] {f : ι set α} (hf : (i : ι), is_lower_set (f i)) :
is_lower_set ( (i : ι), f i)
theorem is_upper_set_Union₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {f : Π (i : ι), κ i set α} (hf : (i : ι) (j : κ i), is_upper_set (f i j)) :
is_upper_set ( (i : ι) (j : κ i), f i j)
theorem is_lower_set_Union₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {f : Π (i : ι), κ i set α} (hf : (i : ι) (j : κ i), is_lower_set (f i j)) :
is_lower_set ( (i : ι) (j : κ i), f i j)
theorem is_upper_set_sUnion {α : Type u_1} [has_le α] {S : set (set α)} (hf : (s : set α), s S ) :
theorem is_lower_set_sUnion {α : Type u_1} [has_le α] {S : set (set α)} (hf : (s : set α), s S ) :
theorem is_upper_set_Inter {α : Type u_1} {ι : Sort u_4} [has_le α] {f : ι set α} (hf : (i : ι), is_upper_set (f i)) :
is_upper_set ( (i : ι), f i)
theorem is_lower_set_Inter {α : Type u_1} {ι : Sort u_4} [has_le α] {f : ι set α} (hf : (i : ι), is_lower_set (f i)) :
is_lower_set ( (i : ι), f i)
theorem is_upper_set_Inter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {f : Π (i : ι), κ i set α} (hf : (i : ι) (j : κ i), is_upper_set (f i j)) :
is_upper_set ( (i : ι) (j : κ i), f i j)
theorem is_lower_set_Inter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {f : Π (i : ι), κ i set α} (hf : (i : ι) (j : κ i), is_lower_set (f i j)) :
is_lower_set ( (i : ι) (j : κ i), f i j)
theorem is_upper_set_sInter {α : Type u_1} [has_le α] {S : set (set α)} (hf : (s : set α), s S ) :
theorem is_lower_set_sInter {α : Type u_1} [has_le α] {S : set (set α)} (hf : (s : set α), s S ) :
@[simp]
theorem is_lower_set_preimage_of_dual_iff {α : Type u_1} [has_le α] {s : set α} :
@[simp]
theorem is_upper_set_preimage_of_dual_iff {α : Type u_1} [has_le α] {s : set α} :
@[simp]
theorem is_lower_set_preimage_to_dual_iff {α : Type u_1} [has_le α] {s : set αᵒᵈ} :
@[simp]
theorem is_upper_set_preimage_to_dual_iff {α : Type u_1} [has_le α] {s : set αᵒᵈ} :
theorem is_upper_set.to_dual {α : Type u_1} [has_le α] {s : set α} :

Alias of the reverse direction of `is_lower_set_preimage_of_dual_iff`.

theorem is_lower_set.to_dual {α : Type u_1} [has_le α] {s : set α} :

Alias of the reverse direction of `is_upper_set_preimage_of_dual_iff`.

theorem is_upper_set.of_dual {α : Type u_1} [has_le α] {s : set αᵒᵈ} :

Alias of the reverse direction of `is_lower_set_preimage_to_dual_iff`.

theorem is_lower_set.of_dual {α : Type u_1} [has_le α] {s : set αᵒᵈ} :

Alias of the reverse direction of `is_upper_set_preimage_to_dual_iff`.

theorem is_upper_set_Ici {α : Type u_1} [preorder α] (a : α) :
theorem is_lower_set_Iic {α : Type u_1} [preorder α] (a : α) :
theorem is_upper_set_Ioi {α : Type u_1} [preorder α] (a : α) :
theorem is_lower_set_Iio {α : Type u_1} [preorder α] (a : α) :
theorem is_upper_set_iff_Ici_subset {α : Type u_1} [preorder α] {s : set α} :
⦃a : α⦄, a s s
theorem is_lower_set_iff_Iic_subset {α : Type u_1} [preorder α] {s : set α} :
⦃a : α⦄, a s s
theorem is_upper_set.Ici_subset {α : Type u_1} [preorder α] {s : set α} :
⦃a : α⦄, a s s

Alias of the forward direction of `is_upper_set_iff_Ici_subset`.

theorem is_lower_set.Iic_subset {α : Type u_1} [preorder α] {s : set α} :
⦃a : α⦄, a s s

Alias of the forward direction of `is_lower_set_iff_Iic_subset`.

theorem is_upper_set.ord_connected {α : Type u_1} [preorder α] {s : set α} (h : is_upper_set s) :
theorem is_lower_set.ord_connected {α : Type u_1} [preorder α] {s : set α} (h : is_lower_set s) :
theorem is_upper_set.preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_upper_set s) {f : β α} (hf : monotone f) :
theorem is_lower_set.preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_lower_set s) {f : β α} (hf : monotone f) :
theorem is_upper_set.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_upper_set s) (f : α ≃o β) :
theorem is_lower_set.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_lower_set s) (f : α ≃o β) :
@[simp]
theorem set.monotone_mem {α : Type u_1} [preorder α] {s : set α} :
monotone (λ (_x : α), _x s)
@[simp]
theorem set.antitone_mem {α : Type u_1} [preorder α] {s : set α} :
antitone (λ (_x : α), _x s)
@[simp]
theorem is_upper_set_set_of {α : Type u_1} [preorder α] {p : α Prop} :
is_upper_set {a : α | p a}
@[simp]
theorem is_lower_set_set_of {α : Type u_1} [preorder α] {p : α Prop} :
is_lower_set {a : α | p a}
theorem is_lower_set.top_mem {α : Type u_1} [preorder α] {s : set α} [order_top α] (hs : is_lower_set s) :
theorem is_upper_set.top_mem {α : Type u_1} [preorder α] {s : set α} [order_top α] (hs : is_upper_set s) :
theorem is_upper_set.not_top_mem {α : Type u_1} [preorder α] {s : set α} [order_top α] (hs : is_upper_set s) :
theorem is_upper_set.bot_mem {α : Type u_1} [preorder α] {s : set α} [order_bot α] (hs : is_upper_set s) :
theorem is_lower_set.bot_mem {α : Type u_1} [preorder α] {s : set α} [order_bot α] (hs : is_lower_set s) :
theorem is_lower_set.not_bot_mem {α : Type u_1} [preorder α] {s : set α} [order_bot α] (hs : is_lower_set s) :
theorem is_upper_set.not_bdd_above {α : Type u_1} [preorder α] {s : set α} [no_max_order α] (hs : is_upper_set s) :
theorem not_bdd_above_Ici {α : Type u_1} [preorder α] (a : α) [no_max_order α] :
theorem not_bdd_above_Ioi {α : Type u_1} [preorder α] (a : α) [no_max_order α] :
theorem is_lower_set.not_bdd_below {α : Type u_1} [preorder α] {s : set α} [no_min_order α] (hs : is_lower_set s) :
theorem not_bdd_below_Iic {α : Type u_1} [preorder α] (a : α) [no_min_order α] :
theorem not_bdd_below_Iio {α : Type u_1} [preorder α] (a : α) [no_min_order α] :
theorem is_upper_set_iff_forall_lt {α : Type u_1} {s : set α} :
⦃a b : α⦄, a < b a s b s
theorem is_lower_set_iff_forall_lt {α : Type u_1} {s : set α} :
⦃a b : α⦄, b < a a s b s
theorem is_upper_set_iff_Ioi_subset {α : Type u_1} {s : set α} :
⦃a : α⦄, a s s
theorem is_lower_set_iff_Iio_subset {α : Type u_1} {s : set α} :
⦃a : α⦄, a s s
theorem is_upper_set.Ioi_subset {α : Type u_1} {s : set α} :
⦃a : α⦄, a s s

Alias of the forward direction of `is_upper_set_iff_Ioi_subset`.

theorem is_lower_set.Iio_subset {α : Type u_1} {s : set α} :
⦃a : α⦄, a s s

Alias of the forward direction of `is_lower_set_iff_Iio_subset`.

theorem is_upper_set.total {α : Type u_1} [linear_order α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
s t t s
theorem is_lower_set.total {α : Type u_1} [linear_order α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
s t t s

### Bundled upper/lower sets #

structure upper_set (α : Type u_6) [has_le α] :
Type u_6

The type of upper sets of an order.

Instances for `upper_set`
structure lower_set (α : Type u_6) [has_le α] :
Type u_6

The type of lower sets of an order.

Instances for `lower_set`
@[protected, instance]
def upper_set.set_like {α : Type u_1} [has_le α] :
α
Equations
@[ext]
theorem upper_set.ext {α : Type u_1} [has_le α] {s t : upper_set α} :
s = t s = t
@[simp]
theorem upper_set.carrier_eq_coe {α : Type u_1} [has_le α] (s : upper_set α) :
@[protected]
theorem upper_set.upper {α : Type u_1} [has_le α] (s : upper_set α) :
@[simp]
theorem upper_set.mem_mk {α : Type u_1} [has_le α] (carrier : set α) (upper' : is_upper_set carrier) {a : α} :
a {carrier := carrier, upper' := upper'} a carrier
@[protected, instance]
def lower_set.set_like {α : Type u_1} [has_le α] :
α
Equations
@[ext]
theorem lower_set.ext {α : Type u_1} [has_le α] {s t : lower_set α} :
s = t s = t
@[simp]
theorem lower_set.carrier_eq_coe {α : Type u_1} [has_le α] (s : lower_set α) :
@[protected]
theorem lower_set.lower {α : Type u_1} [has_le α] (s : lower_set α) :
@[simp]
theorem lower_set.mem_mk {α : Type u_1} [has_le α] (carrier : set α) (lower' : is_lower_set carrier) {a : α} :
a {carrier := carrier, lower' := lower'} a carrier

#### Order #

@[protected, instance]
def upper_set.has_sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_top {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_bot {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_Sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def upper_set.has_Inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
Equations
• upper_set.complete_distrib_lattice = upper_set.complete_distrib_lattice._proof_1 upper_set.complete_distrib_lattice._proof_2 upper_set.complete_distrib_lattice._proof_3 upper_set.complete_distrib_lattice._proof_4 upper_set.complete_distrib_lattice._proof_5 upper_set.complete_distrib_lattice._proof_6 upper_set.complete_distrib_lattice._proof_7
@[protected, instance]
def upper_set.inhabited {α : Type u_1} [has_le α] :
Equations
@[simp, norm_cast]
theorem upper_set.coe_subset_coe {α : Type u_1} [has_le α] {s t : upper_set α} :
s t t s
@[simp, norm_cast]
theorem upper_set.coe_top {α : Type u_1} [has_le α] :
@[simp, norm_cast]
theorem upper_set.coe_bot {α : Type u_1} [has_le α] :
@[simp, norm_cast]
theorem upper_set.coe_eq_univ {α : Type u_1} [has_le α] {s : upper_set α} :
s =
@[simp, norm_cast]
theorem upper_set.coe_eq_empty {α : Type u_1} [has_le α] {s : upper_set α} :
@[simp, norm_cast]
theorem upper_set.coe_sup {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t) = s t
@[simp, norm_cast]
theorem upper_set.coe_inf {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t) = s t
@[simp, norm_cast]
theorem upper_set.coe_Sup {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Sup.Sup S) = (s : (H : s S), s
@[simp, norm_cast]
theorem upper_set.coe_Inf {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Inf.Inf S) = (s : (H : s S), s
@[simp, norm_cast]
theorem upper_set.coe_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem upper_set.coe_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem upper_set.coe_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)
@[simp, norm_cast]
theorem upper_set.coe_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)
@[simp]
theorem upper_set.not_mem_top {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem upper_set.mem_bot {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem upper_set.mem_sup_iff {α : Type u_1} [has_le α] {s t : upper_set α} {a : α} :
a s t a s a t
@[simp]
theorem upper_set.mem_inf_iff {α : Type u_1} [has_le α] {s t : upper_set α} {a : α} :
a s t a s a t
@[simp]
theorem upper_set.mem_Sup_iff {α : Type u_1} [has_le α] {S : set (upper_set α)} {a : α} :
a (s : , s S a s
@[simp]
theorem upper_set.mem_Inf_iff {α : Type u_1} [has_le α] {S : set (upper_set α)} {a : α} :
a (s : (H : s S), a s
@[simp]
theorem upper_set.mem_supr_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι } :
(a (i : ι), f i) (i : ι), a f i
@[simp]
theorem upper_set.mem_infi_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι } :
(a (i : ι), f i) (i : ι), a f i
@[simp]
theorem upper_set.mem_supr₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i } :
(a (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), a f i j
@[simp]
theorem upper_set.mem_infi₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i } :
(a (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), a f i j
@[simp, norm_cast]
theorem upper_set.codisjoint_coe {α : Type u_1} [has_le α] {s t : upper_set α} :
t t
@[protected, instance]
def lower_set.has_sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_top {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_bot {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_Sup {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
def lower_set.has_Inf {α : Type u_1} [has_le α] :
Equations
@[protected, instance]
Equations
• lower_set.complete_distrib_lattice = lower_set.complete_distrib_lattice._proof_1 lower_set.complete_distrib_lattice._proof_2 lower_set.complete_distrib_lattice._proof_3 lower_set.complete_distrib_lattice._proof_4 lower_set.complete_distrib_lattice._proof_5 lower_set.complete_distrib_lattice._proof_6 lower_set.complete_distrib_lattice._proof_7
@[protected, instance]
def lower_set.inhabited {α : Type u_1} [has_le α] :
Equations
@[simp, norm_cast]
theorem lower_set.coe_subset_coe {α : Type u_1} [has_le α] {s t : lower_set α} :
s t s t
@[simp, norm_cast]
theorem lower_set.coe_top {α : Type u_1} [has_le α] :
@[simp, norm_cast]
theorem lower_set.coe_bot {α : Type u_1} [has_le α] :
@[simp, norm_cast]
theorem lower_set.coe_eq_univ {α : Type u_1} [has_le α] {s : lower_set α} :
s =
@[simp, norm_cast]
theorem lower_set.coe_eq_empty {α : Type u_1} [has_le α] {s : lower_set α} :
@[simp, norm_cast]
theorem lower_set.coe_sup {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t) = s t
@[simp, norm_cast]
theorem lower_set.coe_inf {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t) = s t
@[simp, norm_cast]
theorem lower_set.coe_Sup {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Sup.Sup S) = (s : (H : s S), s
@[simp, norm_cast]
theorem lower_set.coe_Inf {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Inf.Inf S) = (s : (H : s S), s
@[simp, norm_cast]
theorem lower_set.coe_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem lower_set.coe_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i) = (i : ι), (f i)
@[simp, norm_cast]
theorem lower_set.coe_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)
@[simp, norm_cast]
theorem lower_set.coe_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), (f i j)
@[simp]
theorem lower_set.mem_top {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem lower_set.not_mem_bot {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem lower_set.mem_sup_iff {α : Type u_1} [has_le α] {s t : lower_set α} {a : α} :
a s t a s a t
@[simp]
theorem lower_set.mem_inf_iff {α : Type u_1} [has_le α] {s t : lower_set α} {a : α} :
a s t a s a t
@[simp]
theorem lower_set.mem_Sup_iff {α : Type u_1} [has_le α] {S : set (lower_set α)} {a : α} :
a (s : (H : s S), a s
@[simp]
theorem lower_set.mem_Inf_iff {α : Type u_1} [has_le α] {S : set (lower_set α)} {a : α} :
a (s : , s S a s
@[simp]
theorem lower_set.mem_supr_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι } :
(a (i : ι), f i) (i : ι), a f i
@[simp]
theorem lower_set.mem_infi_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι } :
(a (i : ι), f i) (i : ι), a f i
@[simp]
theorem lower_set.mem_supr₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i } :
(a (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), a f i j
@[simp]
theorem lower_set.mem_infi₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i } :
(a (i : ι) (j : κ i), f i j) (i : ι) (j : κ i), a f i j
@[simp, norm_cast]
theorem lower_set.disjoint_coe {α : Type u_1} [has_le α] {s t : lower_set α} :
t t

#### Complement #

def upper_set.compl {α : Type u_1} [has_le α] (s : upper_set α) :

The complement of a lower set as an upper set.

Equations
def lower_set.compl {α : Type u_1} [has_le α] (s : lower_set α) :

The complement of a lower set as an upper set.

Equations
@[simp]
theorem upper_set.coe_compl {α : Type u_1} [has_le α] (s : upper_set α) :
@[simp]
theorem upper_set.mem_compl_iff {α : Type u_1} [has_le α] {s : upper_set α} {a : α} :
a s.compl a s
@[simp]
theorem upper_set.compl_compl {α : Type u_1} [has_le α] (s : upper_set α) :
@[simp]
theorem upper_set.compl_le_compl {α : Type u_1} [has_le α] {s t : upper_set α} :
@[protected, simp]
theorem upper_set.compl_sup {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t).compl = s.compl t.compl
@[protected, simp]
theorem upper_set.compl_inf {α : Type u_1} [has_le α] (s t : upper_set α) :
(s t).compl = s.compl t.compl
@[protected, simp]
theorem upper_set.compl_top {α : Type u_1} [has_le α] :
@[protected, simp]
theorem upper_set.compl_bot {α : Type u_1} [has_le α] :
@[protected, simp]
theorem upper_set.compl_Sup {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Sup.Sup S).compl = (s : (H : s S), s.compl
@[protected, simp]
theorem upper_set.compl_Inf {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Inf.Inf S).compl = (s : (H : s S), s.compl
@[protected, simp]
theorem upper_set.compl_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i).compl = (i : ι), (f i).compl
@[protected, simp]
theorem upper_set.compl_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i).compl = (i : ι), (f i).compl
@[simp]
theorem upper_set.compl_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j).compl = (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem upper_set.compl_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j).compl = (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem lower_set.coe_compl {α : Type u_1} [has_le α] (s : lower_set α) :
@[simp]
theorem lower_set.mem_compl_iff {α : Type u_1} [has_le α] {s : lower_set α} {a : α} :
a s.compl a s
@[simp]
theorem lower_set.compl_compl {α : Type u_1} [has_le α] (s : lower_set α) :
@[simp]
theorem lower_set.compl_le_compl {α : Type u_1} [has_le α] {s t : lower_set α} :
@[protected]
theorem lower_set.compl_sup {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t).compl = s.compl t.compl
@[protected]
theorem lower_set.compl_inf {α : Type u_1} [has_le α] (s t : lower_set α) :
(s t).compl = s.compl t.compl
@[protected]
theorem lower_set.compl_top {α : Type u_1} [has_le α] :
@[protected]
theorem lower_set.compl_bot {α : Type u_1} [has_le α] :
@[protected]
theorem lower_set.compl_Sup {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Sup.Sup S).compl = (s : (H : s S), s.compl
@[protected]
theorem lower_set.compl_Inf {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Inf.Inf S).compl = (s : (H : s S), s.compl
@[protected]
theorem lower_set.compl_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i).compl = (i : ι), (f i).compl
@[protected]
theorem lower_set.compl_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι ) :
( (i : ι), f i).compl = (i : ι), (f i).compl
@[simp]
theorem lower_set.compl_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j).compl = (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem lower_set.compl_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} [has_le α] (f : Π (i : ι), κ i ) :
( (i : ι) (j : κ i), f i j).compl = (i : ι) (j : κ i), (f i j).compl
@[simp]
theorem upper_set_iso_lower_set_symm_apply {α : Type u_1} [has_le α] (s : lower_set α) :
@[simp]
theorem upper_set_iso_lower_set_apply {α : Type u_1} [has_le α] (s : upper_set α) :
def upper_set_iso_lower_set {α : Type u_1} [has_le α] :

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

Equations
@[protected, instance]
def upper_set.is_total_le {α : Type u_1} [linear_order α] :
@[protected, instance]
def lower_set.is_total_le {α : Type u_1} [linear_order α] :
@[protected, instance]
noncomputable def upper_set.complete_linear_order {α : Type u_1} [linear_order α] :
Equations
@[protected, instance]
noncomputable def lower_set.complete_linear_order {α : Type u_1} [linear_order α] :
Equations

#### Map #

def upper_set.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
@[simp]
theorem upper_set.symm_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :
@[simp]
theorem upper_set.mem_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α ≃o β} {s : upper_set α} {b : β} :
b s (f.symm) b s
@[simp]
theorem upper_set.map_refl {α : Type u_1} [preorder α] :
@[simp]
theorem upper_set.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] {s : upper_set α} (g : β ≃o γ) (f : α ≃o β) :
@[simp, norm_cast]
theorem upper_set.coe_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : upper_set α) :
( s) = f '' s
def lower_set.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
@[simp]
theorem lower_set.symm_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :
@[simp]
theorem lower_set.mem_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : lower_set α} {f : α ≃o β} {b : β} :
b s (f.symm) b s
@[simp]
theorem lower_set.map_refl {α : Type u_1} [preorder α] :
@[simp]
theorem lower_set.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] {s : lower_set α} (g : β ≃o γ) (f : α ≃o β) :
@[simp, norm_cast]
theorem lower_set.coe_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : lower_set α) :
( s) = f '' s
@[simp]
theorem upper_set.compl_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : upper_set α) :
@[simp]
theorem lower_set.compl_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : lower_set α) :

#### Principal sets #

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

The smallest upper set containing a given element.

Equations
def upper_set.Ioi {α : Type u_1} [preorder α] (a : α) :

The smallest upper set containing a given element.

Equations
@[simp]
theorem upper_set.coe_Ici {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_set.coe_Ioi {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_set.mem_Ici_iff {α : Type u_1} [preorder α] {a b : α} :
a b
@[simp]
theorem upper_set.mem_Ioi_iff {α : Type u_1} [preorder α] {a b : α} :
a < b
@[simp]
theorem upper_set.map_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
@[simp]
theorem upper_set.map_Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
theorem upper_set.Ici_le_Ioi {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_set.Ioi_top {α : Type u_1} [preorder α] [order_top α] :
@[simp]
theorem upper_set.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :
@[simp]
theorem upper_set.Ici_sup {α : Type u_1} (a b : α) :
@[simp]
theorem upper_set.Ici_Sup {α : Type u_1} (S : set α) :
= (a : α) (H : a S),
@[simp]
theorem upper_set.Ici_supr {α : Type u_1} {ι : Sort u_4} (f : ι α) :
upper_set.Ici ( (i : ι), f i) = (i : ι), upper_set.Ici (f i)
@[simp]
theorem upper_set.Ici_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} (f : Π (i : ι), κ i α) :
upper_set.Ici ( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), upper_set.Ici (f i j)
def lower_set.Iic {α : Type u_1} [preorder α] (a : α) :

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

Equations
def lower_set.Iio {α : Type u_1} [preorder α] (a : α) :

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

Equations
@[simp]
theorem lower_set.coe_Iic {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_set.coe_Iio {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_set.mem_Iic_iff {α : Type u_1} [preorder α] {a b : α} :
b a
@[simp]
theorem lower_set.mem_Iio_iff {α : Type u_1} [preorder α] {a b : α} :
b < a
@[simp]
theorem lower_set.map_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
@[simp]
theorem lower_set.map_Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
theorem lower_set.Ioi_le_Ici {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_set.Iic_top {α : Type u_1} [preorder α] [order_top α] :
@[simp]
theorem lower_set.Iio_bot {α : Type u_1} [preorder α] [order_bot α] :
@[simp]
theorem lower_set.Iic_inf {α : Type u_1} (a b : α) :
@[simp]
theorem lower_set.Iic_Inf {α : Type u_1} (S : set α) :
= (a : α) (H : a S),
@[simp]
theorem lower_set.Iic_infi {α : Type u_1} {ι : Sort u_4} (f : ι α) :
lower_set.Iic ( (i : ι), f i) = (i : ι), lower_set.Iic (f i)
@[simp]
theorem lower_set.Iic_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι Sort u_5} (f : Π (i : ι), κ i α) :
lower_set.Iic ( (i : ι) (j : κ i), f i j) = (i : ι) (j : κ i), lower_set.Iic (f i j)
def upper_closure {α : Type u_1} [preorder α] (s : set α) :

The greatest upper set containing a given set.

Equations
def lower_closure {α : Type u_1} [preorder α] (s : set α) :

The least lower set containing a given set.

Equations
@[simp]
theorem mem_upper_closure {α : Type u_1} [preorder α] {s : set α} {x : α} :
(a : α) (H : a s), a x
@[simp]
theorem mem_lower_closure {α : Type u_1} [preorder α] {s : set α} {x : α} :
(a : α) (H : a s), x a
@[norm_cast]
theorem coe_upper_closure {α : Type u_1} [preorder α] (s : set α) :
= (a : α) (H : a s),
@[norm_cast]
theorem coe_lower_closure {α : Type u_1} [preorder α] (s : set α) :
= (a : α) (H : a s),
theorem subset_upper_closure {α : Type u_1} [preorder α] {s : set α} :
theorem subset_lower_closure {α : Type u_1} [preorder α] {s : set α} :
theorem upper_closure_min {α : Type u_1} [preorder α] {s t : set α} (h : s t) (ht : is_upper_set t) :
theorem lower_closure_min {α : Type u_1} [preorder α] {s t : set α} (h : s t) (ht : is_lower_set t) :
@[protected]
theorem is_upper_set.upper_closure {α : Type u_1} [preorder α] {s : set α} (hs : is_upper_set s) :
= s
@[protected]
theorem is_lower_set.lower_closure {α : Type u_1} [preorder α] {s : set α} (hs : is_lower_set s) :
= s
@[protected, simp]
theorem upper_set.upper_closure {α : Type u_1} [preorder α] (s : upper_set α) :
@[protected, simp]
theorem lower_set.lower_closure {α : Type u_1} [preorder α] (s : lower_set α) :
@[simp]
theorem upper_closure_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (f : α ≃o β) :
@[simp]
theorem lower_closure_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (f : α ≃o β) :
@[simp]
theorem upper_set.infi_Ici {α : Type u_1} [preorder α] (s : set α) :
( (a : α) (H : a s), =
@[simp]
theorem lower_set.supr_Iic {α : Type u_1} [preorder α] (s : set α) :
( (a : α) (H : a s), =
theorem gc_upper_closure_coe {α : Type u_1} [preorder α] :
theorem gc_lower_closure_coe {α : Type u_1} [preorder α] :
def gi_upper_closure_coe {α : Type u_1} [preorder α] :

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

Equations
def gi_lower_closure_coe {α : Type u_1} [preorder α] :

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

Equations
theorem upper_closure_anti {α : Type u_1} [preorder α] :
theorem lower_closure_mono {α : Type u_1} [preorder α] :
@[simp]
theorem upper_closure_empty {α : Type u_1} [preorder α] :
@[simp]
theorem lower_closure_empty {α : Type u_1} [preorder α] :
@[simp]
theorem upper_closure_singleton {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem lower_closure_singleton {α : Type u_1} [preorder α] (a : α) :
@[simp]
theorem upper_closure_univ {α : Type u_1} [preorder α] :
@[simp]
theorem lower_closure_univ {α : Type u_1} [preorder α] :
@[simp]
theorem upper_closure_eq_top_iff {α : Type u_1} [preorder α] {s : set α} :
s =
@[simp]
theorem lower_closure_eq_bot_iff {α : Type u_1} [preorder α] {s : set α} :
s =
@[simp]
theorem upper_closure_union {α : Type u_1} [preorder α] (s t : set α) :
@[simp]
theorem lower_closure_union {α : Type u_1} [preorder α] (s t : set α) :
@[simp]
theorem upper_closure_Union {α : Type u_1} {ι : Sort u_4} [preorder α] (f : ι set α) :
upper_closure ( (i : ι), f i) = (i : ι), upper_closure (f i)
@[simp]
theorem lower_closure_Union {α : Type u_1} {ι : Sort u_4} [preorder α] (f : ι set α) :
lower_closure ( (i : ι), f i) = (i : ι), lower_closure (f i)
@[simp]
theorem upper_closure_sUnion {α : Type u_1} [preorder α] (S : set (set α)) :
upper_closure (⋃₀ S) = (s : set α) (H : s S),
@[simp]
theorem lower_closure_sUnion {α : Type u_1} [preorder α] (S : set (set α)) :
lower_closure (⋃₀ S) = (s : set α) (H : s S),
@[simp]
theorem upper_bounds_lower_closure {α : Type u_1} [preorder α] {s : set α} :
@[simp]
theorem lower_bounds_upper_closure {α : Type u_1} [preorder α] {s : set α} :
@[simp]
theorem bdd_above_lower_closure {α : Type u_1} [preorder α] {s : set α} :
@[simp]
theorem bdd_below_upper_closure {α : Type u_1} [preorder α] {s : set α} :
@[protected]
theorem bdd_above.lower_closure {α : Type u_1} [preorder α] {s : set α} :

Alias of the reverse direction of `bdd_above_lower_closure`.

theorem bdd_above.of_lower_closure {α : Type u_1} [preorder α] {s : set α} :

Alias of the forward direction of `bdd_above_lower_closure`.

theorem bdd_below.of_upper_closure {α : Type u_1} [preorder α] {s : set α} :

Alias of the forward direction of `bdd_below_upper_closure`.

@[protected]
theorem bdd_below.upper_closure {α : Type u_1} [preorder α] {s : set α} :

Alias of the reverse direction of `bdd_below_upper_closure`.

### Product #

theorem is_upper_set.prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} {t : set β} (hs : is_upper_set s) (ht : is_upper_set t) :
theorem is_lower_set.prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} {t : set β} (hs : is_lower_set s) (ht : is_lower_set t) :
def upper_set.prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : upper_set α) (t : upper_set β) :
upper_set × β)

The product of two upper sets as an upper set.

Equations
@[simp, norm_cast]
theorem upper_set.coe_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : upper_set α) (t : upper_set β) :
(s ×ˢ t) = s ×ˢ t
@[simp]
theorem upper_set.mem_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {x : α × β} {s : upper_set α} {t : upper_set β} :
x s ×ˢ t x.fst s x.snd t
theorem upper_set.Ici_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α × β) :
@[simp]
theorem upper_set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
@[simp]
theorem upper_set.prod_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : upper_set α) :
@[simp]
theorem upper_set.top_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (t : upper_set β) :
@[simp]
theorem upper_set.bot_prod_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
@[simp]
theorem upper_set.sup_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s₁ s₂ : upper_set α) (t : upper_set β) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem upper_set.prod_sup {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : upper_set α) (t₁ t₂ : upper_set β) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem upper_set.inf_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s₁ s₂ : upper_set α) (t : upper_set β) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem upper_set.prod_inf {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : upper_set α) (t₁ t₂ : upper_set β) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
theorem upper_set.prod_sup_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s₁ s₂ : upper_set α) (t₁ t₂ : upper_set β) :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
theorem upper_set.prod_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : upper_set α} {t₁ t₂ : upper_set β} :
s₁ s₂ t₁ t₂ s₁ ×ˢ t₁ s₂ ×ˢ t₂
theorem upper_set.prod_mono_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : upper_set α} {t : upper_set β} :
s₁ s₂ s₁ ×ˢ t s₂ ×ˢ t
theorem upper_set.prod_mono_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : upper_set α} {t₁ t₂ : upper_set β} :
t₁ t₂ s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem upper_set.prod_self_le_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : upper_set α} :
s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
@[simp]
theorem upper_set.prod_self_lt_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : upper_set α} :
s₁ ×ˢ s₁ < s₂ ×ˢ s₂ s₁ < s₂
theorem upper_set.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : upper_set α} {t₁ t₂ : upper_set β} :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ s₁ s₂ t₁ t₂ s₂ = t₂ =
@[simp]
theorem upper_set.prod_eq_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : upper_set α} {t : upper_set β} :
s ×ˢ t = s = t =
@[simp]
theorem upper_set.codisjoint_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : upper_set α} {t₁ t₂ : upper_set β} :
codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) s₂ t₂
def lower_set.prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : lower_set α) (t : lower_set β) :
lower_set × β)

The product of two lower sets as a lower set.

Equations
@[simp, norm_cast]
theorem lower_set.coe_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : lower_set α) (t : lower_set β) :
(s ×ˢ t) = s ×ˢ t
@[simp]
theorem lower_set.mem_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {x : α × β} {s : lower_set α} {t : lower_set β} :
x s ×ˢ t x.fst s x.snd t
theorem lower_set.Iic_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α × β) :
@[simp]
theorem lower_set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
@[simp]
theorem lower_set.prod_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : lower_set α) :
@[simp]
theorem lower_set.bot_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (t : lower_set β) :
@[simp]
theorem lower_set.top_prod_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
@[simp]
theorem lower_set.inf_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s₁ s₂ : lower_set α) (t : lower_set β) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem lower_set.prod_inf {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : lower_set α) (t₁ t₂ : lower_set β) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem lower_set.sup_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s₁ s₂ : lower_set α) (t : lower_set β) :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
@[simp]
theorem lower_set.prod_sup {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : lower_set α) (t₁ t₂ : lower_set β) :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
theorem lower_set.prod_inf_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s₁ s₂ : lower_set α) (t₁ t₂ : lower_set β) :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
theorem lower_set.prod_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : lower_set α} {t₁ t₂ : lower_set β} :
s₁ s₂ t₁ t₂ s₁ ×ˢ t₁ s₂ ×ˢ t₂
theorem lower_set.prod_mono_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : lower_set α} {t : lower_set β} :
s₁ s₂ s₁ ×ˢ t s₂ ×ˢ t
theorem lower_set.prod_mono_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : lower_set α} {t₁ t₂ : lower_set β} :
t₁ t₂ s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem lower_set.prod_self_le_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : lower_set α} :
s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
@[simp]
theorem lower_set.prod_self_lt_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : lower_set α} :
s₁ ×ˢ s₁ < s₂ ×ˢ s₂ s₁ < s₂
theorem lower_set.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : lower_set α} {t₁ t₂ : lower_set β} :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ s₁ s₂ t₁ t₂ s₁ = t₁ =
@[simp]
theorem lower_set.prod_eq_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : lower_set α} {t : lower_set β} :
s ×ˢ t = s = t =
@[simp]
theorem lower_set.disjoint_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s₁ s₂ : lower_set α} {t₁ t₂ : lower_set β} :
disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) disjoint s₁ s₂ disjoint t₁ t₂
@[simp]
theorem upper_closure_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : set α) (t : set β) :
@[simp]
theorem lower_closure_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : set α) (t : set β) :