mathlib3 documentation

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 #

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 #

source
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
source
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
source
theorem is_upper_set_empty {α : Type u_1} [has_le α] :
is_upper_set ∅
source
theorem is_lower_set_empty {α : Type u_1} [has_le α] :
is_lower_set ∅
source
theorem is_upper_set_univ {α : Type u_1} [has_le α] :
is_upper_set set.univ
source
theorem is_lower_set_univ {α : Type u_1} [has_le α] :
is_lower_set set.univ
source
theorem is_upper_set.compl {α : Type u_1} [has_le α] {s : set α} (hs : is_upper_set s) :
is_lower_set sᶜ
source
theorem is_lower_set.compl {α : Type u_1} [has_le α] {s : set α} (hs : is_lower_set s) :
is_upper_set sᶜ
source
@[simp]
theorem is_upper_set_compl {α : Type u_1} [has_le α] {s : set α} :
is_upper_set sᶜ ↔ is_lower_set s
source
@[simp]
theorem is_lower_set_compl {α : Type u_1} [has_le α] {s : set α} :
is_lower_set sᶜ ↔ is_upper_set s
source
theorem is_upper_set.union {α : Type u_1} [has_le α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
is_upper_set (s ∪ t)
source
theorem is_lower_set.union {α : Type u_1} [has_le α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
is_lower_set (s ∪ t)
source
theorem is_upper_set.inter {α : Type u_1} [has_le α] {s t : set α} (hs : is_upper_set s) (ht : is_upper_set t) :
is_upper_set (s ∩ t)
source
theorem is_lower_set.inter {α : Type u_1} [has_le α] {s t : set α} (hs : is_lower_set s) (ht : is_lower_set t) :
is_lower_set (s ∩ t)
source
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)
source
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)
source
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)
source
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)
source
theorem is_upper_set_sUnion {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s ∈ S → is_upper_set s) :
is_upper_set (⋃₀ S)
source
theorem is_lower_set_sUnion {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s ∈ S → is_lower_set s) :
is_lower_set (⋃₀ S)
source
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)
source
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)
source
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)
source
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)
source
theorem is_upper_set_sInter {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s ∈ S → is_upper_set s) :
is_upper_set (⋂₀ S)
source
theorem is_lower_set_sInter {α : Type u_1} [has_le α] {S : set (set α)} (hf : ∀ (s : set α), s ∈ S → is_lower_set s) :
is_lower_set (⋂₀ S)
source
@[simp]
theorem is_lower_set_preimage_of_dual_iff {α : Type u_1} [has_le α] {s : set α} :
is_lower_set (⇑order_dual.of_dual ⁻¹' s) ↔ is_upper_set s
source
@[simp]
theorem is_upper_set_preimage_of_dual_iff {α : Type u_1} [has_le α] {s : set α} :
is_upper_set (⇑order_dual.of_dual ⁻¹' s) ↔ is_lower_set s
source
@[simp]
theorem is_lower_set_preimage_to_dual_iff {α : Type u_1} [has_le α] {s : set αᵒᵈ} :
is_lower_set (⇑order_dual.to_dual ⁻¹' s) ↔ is_upper_set s
source
@[simp]
theorem is_upper_set_preimage_to_dual_iff {α : Type u_1} [has_le α] {s : set αᵒᵈ} :
is_upper_set (⇑order_dual.to_dual ⁻¹' s) ↔ is_lower_set s
source
theorem is_upper_set.to_dual {α : Type u_1} [has_le α] {s : set α} :
is_upper_set s → is_lower_set (⇑order_dual.of_dual ⁻¹' s)

Alias of the reverse direction of is_lower_set_preimage_of_dual_iff.

source
theorem is_lower_set.to_dual {α : Type u_1} [has_le α] {s : set α} :
is_lower_set s → is_upper_set (⇑order_dual.of_dual ⁻¹' s)

Alias of the reverse direction of is_upper_set_preimage_of_dual_iff.

source
theorem is_upper_set.of_dual {α : Type u_1} [has_le α] {s : set αᵒᵈ} :
is_upper_set s → is_lower_set (⇑order_dual.to_dual ⁻¹' s)

Alias of the reverse direction of is_lower_set_preimage_to_dual_iff.

source
theorem is_lower_set.of_dual {α : Type u_1} [has_le α] {s : set αᵒᵈ} :
is_lower_set s → is_upper_set (⇑order_dual.to_dual ⁻¹' s)

Alias of the reverse direction of is_upper_set_preimage_to_dual_iff.

source
theorem is_upper_set_Ici {α : Type u_1} [preorder α] (a : α) :
is_upper_set (set.Ici a)
source
theorem is_lower_set_Iic {α : Type u_1} [preorder α] (a : α) :
is_lower_set (set.Iic a)
source
theorem is_upper_set_Ioi {α : Type u_1} [preorder α] (a : α) :
is_upper_set (set.Ioi a)
source
theorem is_lower_set_Iio {α : Type u_1} [preorder α] (a : α) :
is_lower_set (set.Iio a)
source
theorem is_upper_set_iff_Ici_subset {α : Type u_1} [preorder α] {s : set α} :
is_upper_set s ↔ ∀ ⦃a : α⦄, a ∈ s → set.Ici a ⊆ s
source
theorem is_lower_set_iff_Iic_subset {α : Type u_1} [preorder α] {s : set α} :
is_lower_set s ↔ ∀ ⦃a : α⦄, a ∈ s → set.Iic a ⊆ s
source
theorem is_upper_set.Ici_subset {α : Type u_1} [preorder α] {s : set α} :
is_upper_set s → ∀ ⦃a : α⦄, a ∈ s → set.Ici a ⊆ s

Alias of the forward direction of is_upper_set_iff_Ici_subset.

source
theorem is_lower_set.Iic_subset {α : Type u_1} [preorder α] {s : set α} :
is_lower_set s → ∀ ⦃a : α⦄, a ∈ s → set.Iic a ⊆ s

Alias of the forward direction of is_lower_set_iff_Iic_subset.

source
theorem is_upper_set.ord_connected {α : Type u_1} [preorder α] {s : set α} (h : is_upper_set s) :
s.ord_connected
source
theorem is_lower_set.ord_connected {α : Type u_1} [preorder α] {s : set α} (h : is_lower_set s) :
s.ord_connected
source
theorem is_upper_set.preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_upper_set s) {f : β → α} (hf : monotone f) :
is_upper_set (f ⁻¹' s)
source
theorem is_lower_set.preimage {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_lower_set s) {f : β → α} (hf : monotone f) :
is_lower_set (f ⁻¹' s)
source
theorem is_upper_set.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_upper_set s) (f : α ≃o β) :
is_upper_set (⇑f '' s)
source
theorem is_lower_set.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (hs : is_lower_set s) (f : α ≃o β) :
is_lower_set (⇑f '' s)
source
@[simp]
theorem set.monotone_mem {α : Type u_1} [preorder α] {s : set α} :
monotone (λ (_x : α), _x ∈ s) ↔ is_upper_set s
source
@[simp]
theorem set.antitone_mem {α : Type u_1} [preorder α] {s : set α} :
antitone (λ (_x : α), _x ∈ s) ↔ is_lower_set s
source
@[simp]
theorem is_upper_set_set_of {α : Type u_1} [preorder α] {p : α → Prop} :
is_upper_set {a : α | p a} ↔ monotone p
source
@[simp]
theorem is_lower_set_set_of {α : Type u_1} [preorder α] {p : α → Prop} :
is_lower_set {a : α | p a} ↔ antitone p
source
theorem is_lower_set.top_mem {α : Type u_1} [preorder α] {s : set α} [order_top α] (hs : is_lower_set s) :
⊤ ∈ s ↔ s = set.univ
source
theorem is_upper_set.top_mem {α : Type u_1} [preorder α] {s : set α} [order_top α] (hs : is_upper_set s) :
⊤ ∈ s ↔ s.nonempty
source
theorem is_upper_set.not_top_mem {α : Type u_1} [preorder α] {s : set α} [order_top α] (hs : is_upper_set s) :
⊤ ∉ s ↔ s = ∅
source
theorem is_upper_set.bot_mem {α : Type u_1} [preorder α] {s : set α} [order_bot α] (hs : is_upper_set s) :
⊥ ∈ s ↔ s = set.univ
source
theorem is_lower_set.bot_mem {α : Type u_1} [preorder α] {s : set α} [order_bot α] (hs : is_lower_set s) :
⊥ ∈ s ↔ s.nonempty
source
theorem is_lower_set.not_bot_mem {α : Type u_1} [preorder α] {s : set α} [order_bot α] (hs : is_lower_set s) :
⊥ ∉ s ↔ s = ∅
source
theorem is_upper_set.not_bdd_above {α : Type u_1} [preorder α] {s : set α} [no_max_order α] (hs : is_upper_set s) :
s.nonempty → ¬bdd_above s
source
theorem not_bdd_above_Ici {α : Type u_1} [preorder α] (a : α) [no_max_order α] :
¬bdd_above (set.Ici a)
source
theorem not_bdd_above_Ioi {α : Type u_1} [preorder α] (a : α) [no_max_order α] :
¬bdd_above (set.Ioi a)
source
theorem is_lower_set.not_bdd_below {α : Type u_1} [preorder α] {s : set α} [no_min_order α] (hs : is_lower_set s) :
s.nonempty → ¬bdd_below s
source
theorem not_bdd_below_Iic {α : Type u_1} [preorder α] (a : α) [no_min_order α] :
¬bdd_below (set.Iic a)
source
theorem not_bdd_below_Iio {α : Type u_1} [preorder α] (a : α) [no_min_order α] :
¬bdd_below (set.Iio a)
source
theorem is_upper_set_iff_forall_lt {α : Type u_1} [partial_order α] {s : set α} :
is_upper_set s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s
source
theorem is_lower_set_iff_forall_lt {α : Type u_1} [partial_order α] {s : set α} :
is_lower_set s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s
source
theorem is_upper_set_iff_Ioi_subset {α : Type u_1} [partial_order α] {s : set α} :
is_upper_set s ↔ ∀ ⦃a : α⦄, a ∈ s → set.Ioi a ⊆ s
source
theorem is_lower_set_iff_Iio_subset {α : Type u_1} [partial_order α] {s : set α} :
is_lower_set s ↔ ∀ ⦃a : α⦄, a ∈ s → set.Iio a ⊆ s
source
theorem is_upper_set.Ioi_subset {α : Type u_1} [partial_order α] {s : set α} :
is_upper_set s → ∀ ⦃a : α⦄, a ∈ s → set.Ioi a ⊆ s

Alias of the forward direction of is_upper_set_iff_Ioi_subset.

source
theorem is_lower_set.Iio_subset {α : Type u_1} [partial_order α] {s : set α} :
is_lower_set s → ∀ ⦃a : α⦄, a ∈ s → set.Iio a ⊆ s

Alias of the forward direction of is_lower_set_iff_Iio_subset.

source
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
source
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 #

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

The type of upper sets of an order.

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

The type of lower sets of an order.

Instances for lower_set
source
@[protected, instance]
def upper_set.set_like {α : Type u_1} [has_le α] :
set_like (upper_set α) α
Equations
source
@[ext]
theorem upper_set.ext {α : Type u_1} [has_le α] {s t : upper_set α} :
↑s = ↑t → s = t
source
@[simp]
theorem upper_set.carrier_eq_coe {α : Type u_1} [has_le α] (s : upper_set α) :
s.carrier = ↑s
source
@[protected]
theorem upper_set.upper {α : Type u_1} [has_le α] (s : upper_set α) :
is_upper_set ↑s
source
@[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
source
@[protected, instance]
def lower_set.set_like {α : Type u_1} [has_le α] :
set_like (lower_set α) α
Equations
source
@[ext]
theorem lower_set.ext {α : Type u_1} [has_le α] {s t : lower_set α} :
↑s = ↑t → s = t
source
@[simp]
theorem lower_set.carrier_eq_coe {α : Type u_1} [has_le α] (s : lower_set α) :
s.carrier = ↑s
source
@[protected]
theorem lower_set.lower {α : Type u_1} [has_le α] (s : lower_set α) :
is_lower_set ↑s
source
@[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 #

source
@[protected, instance]
def upper_set.has_sup {α : Type u_1} [has_le α] :
has_sup (upper_set α)
Equations
source
@[protected, instance]
def upper_set.has_inf {α : Type u_1} [has_le α] :
has_inf (upper_set α)
Equations
source
@[protected, instance]
def upper_set.has_top {α : Type u_1} [has_le α] :
has_top (upper_set α)
Equations
source
@[protected, instance]
def upper_set.has_bot {α : Type u_1} [has_le α] :
has_bot (upper_set α)
Equations
source
@[protected, instance]
def upper_set.has_Sup {α : Type u_1} [has_le α] :
has_Sup (upper_set α)
Equations
source
@[protected, instance]
def upper_set.has_Inf {α : Type u_1} [has_le α] :
has_Inf (upper_set α)
Equations
source
@[protected, instance]
def upper_set.complete_distrib_lattice {α : Type u_1} [has_le α] :
complete_distrib_lattice (upper_set α)
Equations
source
@[protected, instance]
def upper_set.inhabited {α : Type u_1} [has_le α] :
inhabited (upper_set α)
Equations
source
@[simp, norm_cast]
theorem upper_set.coe_subset_coe {α : Type u_1} [has_le α] {s t : upper_set α} :
↑s ⊆ ↑t ↔ t ≤ s
source
@[simp, norm_cast]
theorem upper_set.coe_top {α : Type u_1} [has_le α] :
↑⊤ = ∅
source
@[simp, norm_cast]
theorem upper_set.coe_bot {α : Type u_1} [has_le α] :
↑⊥ = set.univ
source
@[simp, norm_cast]
theorem upper_set.coe_eq_univ {α : Type u_1} [has_le α] {s : upper_set α} :
↑s = set.univ ↔ s = ⊥
source
@[simp, norm_cast]
theorem upper_set.coe_eq_empty {α : Type u_1} [has_le α] {s : upper_set α} :
↑s = ∅ ↔ s = ⊤
source
@[simp, norm_cast]
theorem upper_set.coe_sup {α : Type u_1} [has_le α] (s t : upper_set α) :
↑(s ⊔ t) = ↑s ∩ ↑t
source
@[simp, norm_cast]
theorem upper_set.coe_inf {α : Type u_1} [has_le α] (s t : upper_set α) :
↑(s ⊓ t) = ↑s ∪ ↑t
source
@[simp, norm_cast]
theorem upper_set.coe_Sup {α : Type u_1} [has_le α] (S : set (upper_set α)) :
↑(has_Sup.Sup S) = ⋂ (s : upper_set α) (H : s ∈ S), ↑s
source
@[simp, norm_cast]
theorem upper_set.coe_Inf {α : Type u_1} [has_le α] (S : set (upper_set α)) :
↑(has_Inf.Inf S) = ⋃ (s : upper_set α) (H : s ∈ S), ↑s
source
@[simp, norm_cast]
theorem upper_set.coe_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → upper_set α) :
(↑⨆ (i : ι), f i) = ⋂ (i : ι), ↑(f i)
source
@[simp, norm_cast]
theorem upper_set.coe_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → upper_set α) :
(↑⨅ (i : ι), f i) = ⋃ (i : ι), ↑(f i)
source
@[simp, norm_cast]
theorem upper_set.coe_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → upper_set α) :
(↑⨆ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)
source
@[simp, norm_cast]
theorem upper_set.coe_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → upper_set α) :
(↑⨅ (i : ι) (j : κ i), f i j) = ⋃ (i : ι) (j : κ i), ↑(f i j)
source
@[simp]
theorem upper_set.not_mem_top {α : Type u_1} [has_le α] {a : α} :
a ∉ ⊤
source
@[simp]
theorem upper_set.mem_bot {α : Type u_1} [has_le α] {a : α} :
a ∈ ⊥
source
@[simp]
theorem upper_set.mem_sup_iff {α : Type u_1} [has_le α] {s t : upper_set α} {a : α} :
a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t
source
@[simp]
theorem upper_set.mem_inf_iff {α : Type u_1} [has_le α] {s t : upper_set α} {a : α} :
a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t
source
@[simp]
theorem upper_set.mem_Sup_iff {α : Type u_1} [has_le α] {S : set (upper_set α)} {a : α} :
a ∈ has_Sup.Sup S ↔ ∀ (s : upper_set α), s ∈ S → a ∈ s
source
@[simp]
theorem upper_set.mem_Inf_iff {α : Type u_1} [has_le α] {S : set (upper_set α)} {a : α} :
a ∈ has_Inf.Inf S ↔ ∃ (s : upper_set α) (H : s ∈ S), a ∈ s
source
@[simp]
theorem upper_set.mem_supr_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι → upper_set α} :
(a ∈ ⨆ (i : ι), f i) ↔ ∀ (i : ι), a ∈ f i
source
@[simp]
theorem upper_set.mem_infi_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι → upper_set α} :
(a ∈ ⨅ (i : ι), f i) ↔ ∃ (i : ι), a ∈ f i
source
@[simp]
theorem upper_set.mem_supr₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i → upper_set α} :
(a ∈ ⨆ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
source
@[simp]
theorem upper_set.mem_infi₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i → upper_set α} :
(a ∈ ⨅ (i : ι) (j : κ i), f i j) ↔ ∃ (i : ι) (j : κ i), a ∈ f i j
source
@[simp, norm_cast]
theorem upper_set.codisjoint_coe {α : Type u_1} [has_le α] {s t : upper_set α} :
codisjoint ↑s ↑t ↔ disjoint s t
source
@[protected, instance]
def lower_set.has_sup {α : Type u_1} [has_le α] :
has_sup (lower_set α)
Equations
source
@[protected, instance]
def lower_set.has_inf {α : Type u_1} [has_le α] :
has_inf (lower_set α)
Equations
source
@[protected, instance]
def lower_set.has_top {α : Type u_1} [has_le α] :
has_top (lower_set α)
Equations
source
@[protected, instance]
def lower_set.has_bot {α : Type u_1} [has_le α] :
has_bot (lower_set α)
Equations
source
@[protected, instance]
def lower_set.has_Sup {α : Type u_1} [has_le α] :
has_Sup (lower_set α)
Equations
source
@[protected, instance]
def lower_set.has_Inf {α : Type u_1} [has_le α] :
has_Inf (lower_set α)
Equations
source
@[protected, instance]
def lower_set.complete_distrib_lattice {α : Type u_1} [has_le α] :
complete_distrib_lattice (lower_set α)
Equations
source
@[protected, instance]
def lower_set.inhabited {α : Type u_1} [has_le α] :
inhabited (lower_set α)
Equations
source
@[simp, norm_cast]
theorem lower_set.coe_subset_coe {α : Type u_1} [has_le α] {s t : lower_set α} :
↑s ⊆ ↑t ↔ s ≤ t
source
@[simp, norm_cast]
theorem lower_set.coe_top {α : Type u_1} [has_le α] :
↑⊤ = set.univ
source
@[simp, norm_cast]
theorem lower_set.coe_bot {α : Type u_1} [has_le α] :
↑⊥ = ∅
source
@[simp, norm_cast]
theorem lower_set.coe_eq_univ {α : Type u_1} [has_le α] {s : lower_set α} :
↑s = set.univ ↔ s = ⊤
source
@[simp, norm_cast]
theorem lower_set.coe_eq_empty {α : Type u_1} [has_le α] {s : lower_set α} :
↑s = ∅ ↔ s = ⊥
source
@[simp, norm_cast]
theorem lower_set.coe_sup {α : Type u_1} [has_le α] (s t : lower_set α) :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp, norm_cast]
theorem lower_set.coe_inf {α : Type u_1} [has_le α] (s t : lower_set α) :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp, norm_cast]
theorem lower_set.coe_Sup {α : Type u_1} [has_le α] (S : set (lower_set α)) :
↑(has_Sup.Sup S) = ⋃ (s : lower_set α) (H : s ∈ S), ↑s
source
@[simp, norm_cast]
theorem lower_set.coe_Inf {α : Type u_1} [has_le α] (S : set (lower_set α)) :
↑(has_Inf.Inf S) = ⋂ (s : lower_set α) (H : s ∈ S), ↑s
source
@[simp, norm_cast]
theorem lower_set.coe_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → lower_set α) :
(↑⨆ (i : ι), f i) = ⋃ (i : ι), ↑(f i)
source
@[simp, norm_cast]
theorem lower_set.coe_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → lower_set α) :
(↑⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)
source
@[simp, norm_cast]
theorem lower_set.coe_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → lower_set α) :
(↑⨆ (i : ι) (j : κ i), f i j) = ⋃ (i : ι) (j : κ i), ↑(f i j)
source
@[simp, norm_cast]
theorem lower_set.coe_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → lower_set α) :
(↑⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)
source
@[simp]
theorem lower_set.mem_top {α : Type u_1} [has_le α] {a : α} :
a ∈ ⊤
source
@[simp]
theorem lower_set.not_mem_bot {α : Type u_1} [has_le α] {a : α} :
a ∉ ⊥
source
@[simp]
theorem lower_set.mem_sup_iff {α : Type u_1} [has_le α] {s t : lower_set α} {a : α} :
a ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t
source
@[simp]
theorem lower_set.mem_inf_iff {α : Type u_1} [has_le α] {s t : lower_set α} {a : α} :
a ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t
source
@[simp]
theorem lower_set.mem_Sup_iff {α : Type u_1} [has_le α] {S : set (lower_set α)} {a : α} :
a ∈ has_Sup.Sup S ↔ ∃ (s : lower_set α) (H : s ∈ S), a ∈ s
source
@[simp]
theorem lower_set.mem_Inf_iff {α : Type u_1} [has_le α] {S : set (lower_set α)} {a : α} :
a ∈ has_Inf.Inf S ↔ ∀ (s : lower_set α), s ∈ S → a ∈ s
source
@[simp]
theorem lower_set.mem_supr_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι → lower_set α} :
(a ∈ ⨆ (i : ι), f i) ↔ ∃ (i : ι), a ∈ f i
source
@[simp]
theorem lower_set.mem_infi_iff {α : Type u_1} {ι : Sort u_4} [has_le α] {a : α} {f : ι → lower_set α} :
(a ∈ ⨅ (i : ι), f i) ↔ ∀ (i : ι), a ∈ f i
source
@[simp]
theorem lower_set.mem_supr₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i → lower_set α} :
(a ∈ ⨆ (i : ι) (j : κ i), f i j) ↔ ∃ (i : ι) (j : κ i), a ∈ f i j
source
@[simp]
theorem lower_set.mem_infi₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] {a : α} {f : Π (i : ι), κ i → lower_set α} :
(a ∈ ⨅ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
source
@[simp, norm_cast]
theorem lower_set.disjoint_coe {α : Type u_1} [has_le α] {s t : lower_set α} :
disjoint ↑s ↑t ↔ disjoint s t

Complement #

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

The complement of a lower set as an upper set.

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

The complement of a lower set as an upper set.

Equations
source
@[simp]
theorem upper_set.coe_compl {α : Type u_1} [has_le α] (s : upper_set α) :
↑(s.compl) = (↑s)ᶜ
source
@[simp]
theorem upper_set.mem_compl_iff {α : Type u_1} [has_le α] {s : upper_set α} {a : α} :
a ∈ s.compl ↔ a ∉ s
source
@[simp]
theorem upper_set.compl_compl {α : Type u_1} [has_le α] (s : upper_set α) :
s.compl.compl = s
source
@[simp]
theorem upper_set.compl_le_compl {α : Type u_1} [has_le α] {s t : upper_set α} :
s.compl ≤ t.compl ↔ s ≤ t
source
@[protected, simp]
theorem upper_set.compl_sup {α : Type u_1} [has_le α] (s t : upper_set α) :
(s ⊔ t).compl = s.compl ⊔ t.compl
source
@[protected, simp]
theorem upper_set.compl_inf {α : Type u_1} [has_le α] (s t : upper_set α) :
(s ⊓ t).compl = s.compl ⊓ t.compl
source
@[protected, simp]
theorem upper_set.compl_top {α : Type u_1} [has_le α] :
⊤.compl = ⊤
source
@[protected, simp]
theorem upper_set.compl_bot {α : Type u_1} [has_le α] :
⊥.compl = ⊥
source
@[protected, simp]
theorem upper_set.compl_Sup {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Sup.Sup S).compl = ⨆ (s : upper_set α) (H : s ∈ S), s.compl
source
@[protected, simp]
theorem upper_set.compl_Inf {α : Type u_1} [has_le α] (S : set (upper_set α)) :
(has_Inf.Inf S).compl = ⨅ (s : upper_set α) (H : s ∈ S), s.compl
source
@[protected, simp]
theorem upper_set.compl_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → upper_set α) :
(⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
source
@[protected, simp]
theorem upper_set.compl_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → upper_set α) :
(⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
source
@[simp]
theorem upper_set.compl_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → upper_set α) :
(⨆ (i : ι) (j : κ i), f i j).compl = ⨆ (i : ι) (j : κ i), (f i j).compl
source
@[simp]
theorem upper_set.compl_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → upper_set α) :
(⨅ (i : ι) (j : κ i), f i j).compl = ⨅ (i : ι) (j : κ i), (f i j).compl
source
@[simp]
theorem lower_set.coe_compl {α : Type u_1} [has_le α] (s : lower_set α) :
↑(s.compl) = (↑s)ᶜ
source
@[simp]
theorem lower_set.mem_compl_iff {α : Type u_1} [has_le α] {s : lower_set α} {a : α} :
a ∈ s.compl ↔ a ∉ s
source
@[simp]
theorem lower_set.compl_compl {α : Type u_1} [has_le α] (s : lower_set α) :
s.compl.compl = s
source
@[simp]
theorem lower_set.compl_le_compl {α : Type u_1} [has_le α] {s t : lower_set α} :
s.compl ≤ t.compl ↔ s ≤ t
source
@[protected]
theorem lower_set.compl_sup {α : Type u_1} [has_le α] (s t : lower_set α) :
(s ⊔ t).compl = s.compl ⊔ t.compl
source
@[protected]
theorem lower_set.compl_inf {α : Type u_1} [has_le α] (s t : lower_set α) :
(s ⊓ t).compl = s.compl ⊓ t.compl
source
@[protected]
theorem lower_set.compl_top {α : Type u_1} [has_le α] :
⊤.compl = ⊤
source
@[protected]
theorem lower_set.compl_bot {α : Type u_1} [has_le α] :
⊥.compl = ⊥
source
@[protected]
theorem lower_set.compl_Sup {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Sup.Sup S).compl = ⨆ (s : lower_set α) (H : s ∈ S), s.compl
source
@[protected]
theorem lower_set.compl_Inf {α : Type u_1} [has_le α] (S : set (lower_set α)) :
(has_Inf.Inf S).compl = ⨅ (s : lower_set α) (H : s ∈ S), s.compl
source
@[protected]
theorem lower_set.compl_supr {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → lower_set α) :
(⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl
source
@[protected]
theorem lower_set.compl_infi {α : Type u_1} {ι : Sort u_4} [has_le α] (f : ι → lower_set α) :
(⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl
source
@[simp]
theorem lower_set.compl_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → lower_set α) :
(⨆ (i : ι) (j : κ i), f i j).compl = ⨆ (i : ι) (j : κ i), (f i j).compl
source
@[simp]
theorem lower_set.compl_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [has_le α] (f : Π (i : ι), κ i → lower_set α) :
(⨅ (i : ι) (j : κ i), f i j).compl = ⨅ (i : ι) (j : κ i), (f i j).compl
source
@[simp]
theorem upper_set_iso_lower_set_symm_apply {α : Type u_1} [has_le α] (s : lower_set α) :
⇑(rel_iso.symm upper_set_iso_lower_set) s = s.compl
source
@[simp]
theorem upper_set_iso_lower_set_apply {α : Type u_1} [has_le α] (s : upper_set α) :
⇑upper_set_iso_lower_set s = s.compl
source
def upper_set_iso_lower_set {α : Type u_1} [has_le α] :
upper_set α ≃o lower_set α

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

Equations
source
@[protected, instance]
def upper_set.is_total_le {α : Type u_1} [linear_order α] :
is_total (upper_set α) has_le.le
source
@[protected, instance]
def lower_set.is_total_le {α : Type u_1} [linear_order α] :
is_total (lower_set α) has_le.le
source
@[protected, instance]
noncomputable def upper_set.complete_linear_order {α : Type u_1} [linear_order α] :
complete_linear_order (upper_set α)
Equations
source
@[protected, instance]
noncomputable def lower_set.complete_linear_order {α : Type u_1} [linear_order α] :
complete_linear_order (lower_set α)
Equations

Map #

source
def upper_set.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :
upper_set α ≃o upper_set β

An order isomorphism of preorders induces an order isomorphism of their upper sets.

Equations
source
@[simp]
theorem upper_set.symm_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :
(upper_set.map f).symm = upper_set.map f.symm
source
@[simp]
theorem upper_set.mem_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α ≃o β} {s : upper_set α} {b : β} :
b ∈ ⇑(upper_set.map f) s ↔ ⇑(f.symm) b ∈ s
source
@[simp]
theorem upper_set.map_refl {α : Type u_1} [preorder α] :
upper_set.map (order_iso.refl α) = order_iso.refl (upper_set α)
source
@[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 β) :
⇑(upper_set.map g) (⇑(upper_set.map f) s) = ⇑(upper_set.map (f.trans g)) s
source
@[simp, norm_cast]
theorem upper_set.coe_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : upper_set α) :
↑(⇑(upper_set.map f) s) = ⇑f '' ↑s
source
def lower_set.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :
lower_set α ≃o lower_set β

An order isomorphism of preorders induces an order isomorphism of their lower sets.

Equations
source
@[simp]
theorem lower_set.symm_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :
(lower_set.map f).symm = lower_set.map f.symm
source
@[simp]
theorem lower_set.mem_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : lower_set α} {f : α ≃o β} {b : β} :
b ∈ ⇑(lower_set.map f) s ↔ ⇑(f.symm) b ∈ s
source
@[simp]
theorem lower_set.map_refl {α : Type u_1} [preorder α] :
lower_set.map (order_iso.refl α) = order_iso.refl (lower_set α)
source
@[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 β) :
⇑(lower_set.map g) (⇑(lower_set.map f) s) = ⇑(lower_set.map (f.trans g)) s
source
@[simp, norm_cast]
theorem lower_set.coe_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : lower_set α) :
↑(⇑(lower_set.map f) s) = ⇑f '' ↑s
source
@[simp]
theorem upper_set.compl_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : upper_set α) :
(⇑(upper_set.map f) s).compl = ⇑(lower_set.map f) s.compl
source
@[simp]
theorem lower_set.compl_map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (s : lower_set α) :
(⇑(lower_set.map f) s).compl = ⇑(upper_set.map f) s.compl

Principal sets #

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

The smallest upper set containing a given element.

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

The smallest upper set containing a given element.

Equations
source
@[simp]
theorem upper_set.coe_Ici {α : Type u_1} [preorder α] (a : α) :
↑(upper_set.Ici a) = set.Ici a
source
@[simp]
theorem upper_set.coe_Ioi {α : Type u_1} [preorder α] (a : α) :
↑(upper_set.Ioi a) = set.Ioi a
source
@[simp]
theorem upper_set.mem_Ici_iff {α : Type u_1} [preorder α] {a b : α} :
b ∈ upper_set.Ici a ↔ a ≤ b
source
@[simp]
theorem upper_set.mem_Ioi_iff {α : Type u_1} [preorder α] {a b : α} :
b ∈ upper_set.Ioi a ↔ a < b
source
@[simp]
theorem upper_set.map_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
⇑(upper_set.map f) (upper_set.Ici a) = upper_set.Ici (⇑f a)
source
@[simp]
theorem upper_set.map_Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
⇑(upper_set.map f) (upper_set.Ioi a) = upper_set.Ioi (⇑f a)
source
theorem upper_set.Ici_le_Ioi {α : Type u_1} [preorder α] (a : α) :
upper_set.Ici a ≤ upper_set.Ioi a
source
@[simp]
theorem upper_set.Ioi_top {α : Type u_1} [preorder α] [order_top α] :
upper_set.Ioi ⊤ = ⊤
source
@[simp]
theorem upper_set.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :
upper_set.Ici ⊥ = ⊥
source
@[simp]
theorem upper_set.Ici_sup {α : Type u_1} [semilattice_sup α] (a b : α) :
upper_set.Ici (a ⊔ b) = upper_set.Ici a ⊔ upper_set.Ici b
source
@[simp]
theorem upper_set.Ici_Sup {α : Type u_1} [complete_lattice α] (S : set α) :
upper_set.Ici (has_Sup.Sup S) = ⨆ (a : α) (H : a ∈ S), upper_set.Ici a
source
@[simp]
theorem upper_set.Ici_supr {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (f : ι → α) :
upper_set.Ici (⨆ (i : ι), f i) = ⨆ (i : ι), upper_set.Ici (f i)
source
@[simp]
theorem upper_set.Ici_supr₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [complete_lattice α] (f : Π (i : ι), κ i → α) :
upper_set.Ici (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), upper_set.Ici (f i j)
source
def lower_set.Iic {α : Type u_1} [preorder α] (a : α) :
lower_set α

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

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

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

Equations
source
@[simp]
theorem lower_set.coe_Iic {α : Type u_1} [preorder α] (a : α) :
↑(lower_set.Iic a) = set.Iic a
source
@[simp]
theorem lower_set.coe_Iio {α : Type u_1} [preorder α] (a : α) :
↑(lower_set.Iio a) = set.Iio a
source
@[simp]
theorem lower_set.mem_Iic_iff {α : Type u_1} [preorder α] {a b : α} :
b ∈ lower_set.Iic a ↔ b ≤ a
source
@[simp]
theorem lower_set.mem_Iio_iff {α : Type u_1} [preorder α] {a b : α} :
b ∈ lower_set.Iio a ↔ b < a
source
@[simp]
theorem lower_set.map_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
⇑(lower_set.map f) (lower_set.Iic a) = lower_set.Iic (⇑f a)
source
@[simp]
theorem lower_set.map_Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) (a : α) :
⇑(lower_set.map f) (lower_set.Iio a) = lower_set.Iio (⇑f a)
source
theorem lower_set.Ioi_le_Ici {α : Type u_1} [preorder α] (a : α) :
set.Ioi a ≤ set.Ici a
source
@[simp]
theorem lower_set.Iic_top {α : Type u_1} [preorder α] [order_top α] :
lower_set.Iic ⊤ = ⊤
source
@[simp]
theorem lower_set.Iio_bot {α : Type u_1} [preorder α] [order_bot α] :
lower_set.Iio ⊥ = ⊥
source
@[simp]
theorem lower_set.Iic_inf {α : Type u_1} [semilattice_inf α] (a b : α) :
lower_set.Iic (a ⊓ b) = lower_set.Iic a ⊓ lower_set.Iic b
source
@[simp]
theorem lower_set.Iic_Inf {α : Type u_1} [complete_lattice α] (S : set α) :
lower_set.Iic (has_Inf.Inf S) = ⨅ (a : α) (H : a ∈ S), lower_set.Iic a
source
@[simp]
theorem lower_set.Iic_infi {α : Type u_1} {ι : Sort u_4} [complete_lattice α] (f : ι → α) :
lower_set.Iic (⨅ (i : ι), f i) = ⨅ (i : ι), lower_set.Iic (f i)
source
@[simp]
theorem lower_set.Iic_infi₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [complete_lattice α] (f : Π (i : ι), κ i → α) :
lower_set.Iic (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), lower_set.Iic (f i j)
source
def upper_closure {α : Type u_1} [preorder α] (s : set α) :
upper_set α

The greatest upper set containing a given set.

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

The least lower set containing a given set.

Equations
source
@[simp]
theorem mem_upper_closure {α : Type u_1} [preorder α] {s : set α} {x : α} :
x ∈ upper_closure s ↔ ∃ (a : α) (H : a ∈ s), a ≤ x
source
@[simp]
theorem mem_lower_closure {α : Type u_1} [preorder α] {s : set α} {x : α} :
x ∈ lower_closure s ↔ ∃ (a : α) (H : a ∈ s), x ≤ a
source
@[norm_cast]
theorem coe_upper_closure {α : Type u_1} [preorder α] (s : set α) :
↑(upper_closure s) = ⋃ (a : α) (H : a ∈ s), set.Ici a
source
@[norm_cast]
theorem coe_lower_closure {α : Type u_1} [preorder α] (s : set α) :
↑(lower_closure s) = ⋃ (a : α) (H : a ∈ s), set.Iic a
source
theorem subset_upper_closure {α : Type u_1} [preorder α] {s : set α} :
s ⊆ ↑(upper_closure s)
source
theorem subset_lower_closure {α : Type u_1} [preorder α] {s : set α} :
s ⊆ ↑(lower_closure s)
source
theorem upper_closure_min {α : Type u_1} [preorder α] {s t : set α} (h : s ⊆ t) (ht : is_upper_set t) :
↑(upper_closure s) ⊆ t
source
theorem lower_closure_min {α : Type u_1} [preorder α] {s t : set α} (h : s ⊆ t) (ht : is_lower_set t) :
↑(lower_closure s) ⊆ t
source
@[protected]
theorem is_upper_set.upper_closure {α : Type u_1} [preorder α] {s : set α} (hs : is_upper_set s) :
↑(upper_closure s) = s
source
@[protected]
theorem is_lower_set.lower_closure {α : Type u_1} [preorder α] {s : set α} (hs : is_lower_set s) :
↑(lower_closure s) = s
source
@[protected, simp]
theorem upper_set.upper_closure {α : Type u_1} [preorder α] (s : upper_set α) :
upper_closure ↑s = s
source
@[protected, simp]
theorem lower_set.lower_closure {α : Type u_1} [preorder α] (s : lower_set α) :
lower_closure ↑s = s
source
@[simp]
theorem upper_closure_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (f : α ≃o β) :
upper_closure (⇑f '' s) = ⇑(upper_set.map f) (upper_closure s)
source
@[simp]
theorem lower_closure_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {s : set α} (f : α ≃o β) :
lower_closure (⇑f '' s) = ⇑(lower_set.map f) (lower_closure s)
source
@[simp]
theorem upper_set.infi_Ici {α : Type u_1} [preorder α] (s : set α) :
(⨅ (a : α) (H : a ∈ s), upper_set.Ici a) = upper_closure s
source
@[simp]
theorem lower_set.supr_Iic {α : Type u_1} [preorder α] (s : set α) :
(⨆ (a : α) (H : a ∈ s), lower_set.Iic a) = lower_closure s
source
theorem gc_upper_closure_coe {α : Type u_1} [preorder α] :
galois_connection (⇑order_dual.to_dual ∘ upper_closure) (coe ∘ ⇑order_dual.of_dual)
source
theorem gc_lower_closure_coe {α : Type u_1} [preorder α] :
galois_connection lower_closure coe
source
def gi_upper_closure_coe {α : Type u_1} [preorder α] :
galois_insertion (⇑order_dual.to_dual ∘ upper_closure) (coe ∘ ⇑order_dual.of_dual)

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

Equations
source
def gi_lower_closure_coe {α : Type u_1} [preorder α] :
galois_insertion lower_closure coe

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

Equations
source
theorem upper_closure_anti {α : Type u_1} [preorder α] :
antitone upper_closure
source
theorem lower_closure_mono {α : Type u_1} [preorder α] :
monotone lower_closure
source
@[simp]
theorem upper_closure_empty {α : Type u_1} [preorder α] :
upper_closure ∅ = ⊤
source
@[simp]
theorem lower_closure_empty {α : Type u_1} [preorder α] :
lower_closure ∅ = ⊥
source
@[simp]
theorem upper_closure_singleton {α : Type u_1} [preorder α] (a : α) :
upper_closure {a} = upper_set.Ici a
source
@[simp]
theorem lower_closure_singleton {α : Type u_1} [preorder α] (a : α) :
lower_closure {a} = lower_set.Iic a
source
@[simp]
theorem upper_closure_univ {α : Type u_1} [preorder α] :
upper_closure set.univ = ⊥
source
@[simp]
theorem lower_closure_univ {α : Type u_1} [preorder α] :
lower_closure set.univ = ⊤
source
@[simp]
theorem upper_closure_eq_top_iff {α : Type u_1} [preorder α] {s : set α} :
upper_closure s = ⊤ ↔ s = ∅
source
@[simp]
theorem lower_closure_eq_bot_iff {α : Type u_1} [preorder α] {s : set α} :
lower_closure s = ⊥ ↔ s = ∅
source
@[simp]
theorem upper_closure_union {α : Type u_1} [preorder α] (s t : set α) :
upper_closure (s ∪ t) = upper_closure s ⊓ upper_closure t
source
@[simp]
theorem lower_closure_union {α : Type u_1} [preorder α] (s t : set α) :
lower_closure (s ∪ t) = lower_closure s ⊔ lower_closure t
source
@[simp]
theorem upper_closure_Union {α : Type u_1} {ι : Sort u_4} [preorder α] (f : ι → set α) :
upper_closure (⋃ (i : ι), f i) = ⨅ (i : ι), upper_closure (f i)
source
@[simp]
theorem lower_closure_Union {α : Type u_1} {ι : Sort u_4} [preorder α] (f : ι → set α) :
lower_closure (⋃ (i : ι), f i) = ⨆ (i : ι), lower_closure (f i)
source
@[simp]
theorem upper_closure_sUnion {α : Type u_1} [preorder α] (S : set (set α)) :
upper_closure (⋃₀ S) = ⨅ (s : set α) (H : s ∈ S), upper_closure s
source
@[simp]
theorem lower_closure_sUnion {α : Type u_1} [preorder α] (S : set (set α)) :
lower_closure (⋃₀ S) = ⨆ (s : set α) (H : s ∈ S), lower_closure s
source
theorem set.ord_connected.upper_closure_inter_lower_closure {α : Type u_1} [preorder α] {s : set α} (h : s.ord_connected) :
↑(upper_closure s) ∩ ↑(lower_closure s) = s
source
theorem ord_connected_iff_upper_closure_inter_lower_closure {α : Type u_1} [preorder α] {s : set α} :
s.ord_connected ↔ ↑(upper_closure s) ∩ ↑(lower_closure s) = s
source
@[simp]
theorem upper_bounds_lower_closure {α : Type u_1} [preorder α] {s : set α} :
upper_bounds ↑(lower_closure s) = upper_bounds s
source
@[simp]
theorem lower_bounds_upper_closure {α : Type u_1} [preorder α] {s : set α} :
lower_bounds ↑(upper_closure s) = lower_bounds s
source
@[simp]
theorem bdd_above_lower_closure {α : Type u_1} [preorder α] {s : set α} :
bdd_above ↑(lower_closure s) ↔ bdd_above s
source
@[simp]
theorem bdd_below_upper_closure {α : Type u_1} [preorder α] {s : set α} :
bdd_below ↑(upper_closure s) ↔ bdd_below s
source
@[protected]
theorem bdd_above.lower_closure {α : Type u_1} [preorder α] {s : set α} :
bdd_above s → bdd_above ↑(lower_closure s)

Alias of the reverse direction of bdd_above_lower_closure.

source
theorem bdd_above.of_lower_closure {α : Type u_1} [preorder α] {s : set α} :
bdd_above ↑(lower_closure s) → bdd_above s

Alias of the forward direction of bdd_above_lower_closure.

source
theorem bdd_below.of_upper_closure {α : Type u_1} [preorder α] {s : set α} :
bdd_below ↑(upper_closure s) → bdd_below s

Alias of the forward direction of bdd_below_upper_closure.

source
@[protected]
theorem bdd_below.upper_closure {α : Type u_1} [preorder α] {s : set α} :
bdd_below s → bdd_below ↑(upper_closure s)

Alias of the reverse direction of bdd_below_upper_closure.

Product #

source
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) :
is_upper_set (s ×ˢ t)
source
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) :
is_lower_set (s ×ˢ t)
source
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
source
@[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
source
@[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
source
theorem upper_set.Ici_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α × β) :
upper_set.Ici x = upper_set.Ici x.fst ×ˢ upper_set.Ici x.snd
source
@[simp]
theorem upper_set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
upper_set.Ici a ×ˢ upper_set.Ici b = upper_set.Ici (a, b)
source
@[simp]
theorem upper_set.prod_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : upper_set α) :
s ×ˢ ⊤ = ⊤
source
@[simp]
theorem upper_set.top_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (t : upper_set β) :
⊤ ×ˢ t = ⊤
source
@[simp]
theorem upper_set.bot_prod_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
⊥ ×ˢ ⊥ = ⊥
source
@[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
source
@[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₂
source
@[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
source
@[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₂
source
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₂)
source
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₂
source
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
source
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₂
source
@[simp]
theorem upper_set.prod_self_le_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : upper_set α} :
s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
source
@[simp]
theorem upper_set.prod_self_lt_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : upper_set α} :
s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
source
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₂ = ⊤
source
@[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 = ⊤
source
@[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₂) ↔ codisjoint s₁ s₂ ∨ codisjoint t₁ t₂
source
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
source
@[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
source
@[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
source
theorem lower_set.Iic_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (x : α × β) :
lower_set.Iic x = lower_set.Iic x.fst ×ˢ lower_set.Iic x.snd
source
@[simp]
theorem lower_set.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a : α) (b : β) :
lower_set.Iic a ×ˢ lower_set.Iic b = lower_set.Iic (a, b)
source
@[simp]
theorem lower_set.prod_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : lower_set α) :
s ×ˢ ⊥ = ⊥
source
@[simp]
theorem lower_set.bot_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (t : lower_set β) :
⊥ ×ˢ t = ⊥
source
@[simp]
theorem lower_set.top_prod_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
⊤ ×ˢ ⊤ = ⊤
source
@[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
source
@[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₂
source
@[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
source
@[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₂
source
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₂)
source
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₂
source
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
source
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₂
source
@[simp]
theorem lower_set.prod_self_le_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : lower_set α} :
s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
source
@[simp]
theorem lower_set.prod_self_lt_prod_self {α : Type u_1} [preorder α] {s₁ s₂ : lower_set α} :
s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
source
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₁ = ⊥
source
@[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 = ⊥
source
@[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₂
source
@[simp]
theorem upper_closure_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : set α) (t : set β) :
upper_closure (s ×ˢ t) = upper_closure s ×ˢ upper_closure t
source
@[simp]
theorem lower_closure_prod {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (s : set α) (t : set β) :
lower_closure (s ×ˢ t) = lower_closure s ×ˢ lower_closure t