Documentation

def IsUpperSet {α : Type u_1} [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

IsUpperSet s = ∀ ⦃a b : α⦄, a ≤ b → a ∈ s → b ∈ s

Instances For

def IsLowerSet {α : Type u_1} [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

IsLowerSet s = ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s

Instances For

theorem isUpperSet_empty {α : Type u_1} [LE α] :

IsUpperSet ∅

theorem isLowerSet_empty {α : Type u_1} [LE α] :

IsLowerSet ∅

theorem isUpperSet_univ {α : Type u_1} [LE α] :

IsUpperSet Set.univ

theorem isLowerSet_univ {α : Type u_1} [LE α] :

IsLowerSet Set.univ

theorem IsUpperSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : IsUpperSet s) :

IsLowerSet sᶜ

theorem IsLowerSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : IsLowerSet s) :

IsUpperSet sᶜ

@[simp]

theorem isUpperSet_compl {α : Type u_1} [LE α] {s : Set α} :

IsUpperSet sᶜ ↔ IsLowerSet s

@[simp]

theorem isLowerSet_compl {α : Type u_1} [LE α] {s : Set α} :

IsLowerSet sᶜ ↔ IsUpperSet s

theorem IsUpperSet.union {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :

IsUpperSet (s ∪ t)

theorem IsLowerSet.union {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :

IsLowerSet (s ∪ t)

theorem IsUpperSet.inter {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :

IsUpperSet (s ∩ t)

theorem IsLowerSet.inter {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :

IsLowerSet (s ∩ t)

theorem isUpperSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ (s : Set α), s ∈ S → IsUpperSet s) :

IsUpperSet (⋃₀ S)

theorem isLowerSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ (s : Set α), s ∈ S → IsLowerSet s) :

IsLowerSet (⋃₀ S)

theorem isUpperSet_iUnion {α : Type u_1} {ι : Sort u_4} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsUpperSet (f i)) :

IsUpperSet (⋃ (i : ι), f i)

theorem isLowerSet_iUnion {α : Type u_1} {ι : Sort u_4} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsLowerSet (f i)) :

IsLowerSet (⋃ (i : ι), f i)

theorem isUpperSet_iUnion₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {f : (i : ι) → κ i → Set α} (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 : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)) :

IsLowerSet (⋃ (i : ι) (j : κ i), f i j)

theorem isUpperSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ (s : Set α), s ∈ S → IsUpperSet s) :

IsUpperSet (⋂₀ S)

theorem isLowerSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ (s : Set α), s ∈ S → IsLowerSet s) :

IsLowerSet (⋂₀ S)

theorem isUpperSet_iInter {α : Type u_1} {ι : Sort u_4} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsUpperSet (f i)) :

IsUpperSet (⋂ (i : ι), f i)

theorem isLowerSet_iInter {α : Type u_1} {ι : Sort u_4} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsLowerSet (f i)) :

IsLowerSet (⋂ (i : ι), f i)

theorem isUpperSet_iInter₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {f : (i : ι) → κ i → Set α} (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 : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)) :

IsLowerSet (⋂ (i : ι) (j : κ i), f i j)

@[simp]

theorem isLowerSet_preimage_ofDual_iff {α : Type u_1} [LE α] {s : Set α} :

IsLowerSet (↑OrderDual.ofDual ⁻¹' s) ↔ IsUpperSet s

@[simp]

theorem isUpperSet_preimage_ofDual_iff {α : Type u_1} [LE α] {s : Set α} :

IsUpperSet (↑OrderDual.ofDual ⁻¹' s) ↔ IsLowerSet s

@[simp]

theorem isLowerSet_preimage_toDual_iff {α : Type u_1} [LE α] {s : Set αᵒᵈ} :

IsLowerSet (↑OrderDual.toDual ⁻¹' s) ↔ IsUpperSet s

@[simp]

theorem isUpperSet_preimage_toDual_iff {α : Type u_1} [LE α] {s : Set αᵒᵈ} :

IsUpperSet (↑OrderDual.toDual ⁻¹' s) ↔ IsLowerSet s

theorem IsUpperSet.toDual {α : Type u_1} [LE α] {s : Set α} :

IsUpperSet s → IsLowerSet (↑OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of isLowerSet_preimage_ofDual_iff.

theorem IsLowerSet.toDual {α : Type u_1} [LE α] {s : Set α} :

IsLowerSet s → IsUpperSet (↑OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of isUpperSet_preimage_ofDual_iff.

theorem IsUpperSet.ofDual {α : Type u_1} [LE α] {s : Set αᵒᵈ} :

IsUpperSet s → IsLowerSet (↑OrderDual.toDual ⁻¹' s)

Alias of the reverse direction of isLowerSet_preimage_toDual_iff.

theorem IsLowerSet.ofDual {α : Type u_1} [LE α] {s : Set αᵒᵈ} :

IsLowerSet s → IsUpperSet (↑OrderDual.toDual ⁻¹' s)

Alias of the reverse direction of isUpperSet_preimage_toDual_iff.

theorem isUpperSet_Ici {α : Type u_1} [Preorder α] (a : α) :

IsUpperSet (Set.Ici a)

theorem isLowerSet_Iic {α : Type u_1} [Preorder α] (a : α) :

IsLowerSet (Set.Iic a)

theorem isUpperSet_Ioi {α : Type u_1} [Preorder α] (a : α) :

IsUpperSet (Set.Ioi a)

theorem isLowerSet_Iio {α : Type u_1} [Preorder α] (a : α) :

IsLowerSet (Set.Iio a)

theorem isUpperSet_iff_Ici_subset {α : Type u_1} [Preorder α] {s : Set α} :

IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Ici a ⊆ s

theorem isLowerSet_iff_Iic_subset {α : Type u_1} [Preorder α] {s : Set α} :

IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Iic a ⊆ s

theorem IsUpperSet.Ici_subset {α : Type u_1} [Preorder α] {s : Set α} :

IsUpperSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Ici a ⊆ s

Alias of the forward direction of isUpperSet_iff_Ici_subset.

theorem IsLowerSet.Iic_subset {α : Type u_1} [Preorder α] {s : Set α} :

IsLowerSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Iic a ⊆ s

Alias of the forward direction of isLowerSet_iff_Iic_subset.

theorem IsUpperSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) :

Set.OrdConnected s

theorem IsLowerSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) :

Set.OrdConnected s

theorem IsUpperSet.preimage {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsUpperSet s) {f : β → α} (hf : Monotone f) :

IsUpperSet (f ⁻¹' s)

theorem IsLowerSet.preimage {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsLowerSet s) {f : β → α} (hf : Monotone f) :

IsLowerSet (f ⁻¹' s)

theorem IsUpperSet.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsUpperSet s) (f : α ≃o β) :

IsUpperSet (↑f '' s)

theorem IsLowerSet.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsLowerSet s) (f : α ≃o β) :

IsLowerSet (↑f '' s)

@[simp]

theorem Set.monotone_mem {α : Type u_1} [Preorder α] {s : Set α} :

(Monotone fun x => x ∈ s) ↔ IsUpperSet s

@[simp]

theorem Set.antitone_mem {α : Type u_1} [Preorder α] {s : Set α} :

(Antitone fun x => x ∈ s) ↔ IsLowerSet s

@[simp]

theorem isUpperSet_setOf {α : Type u_1} [Preorder α] {p : α → Prop} :

IsUpperSet {a | p a} ↔ Monotone p

@[simp]

theorem isLowerSet_setOf {α : Type u_1} [Preorder α] {p : α → Prop} :

IsLowerSet {a | p a} ↔ Antitone p

theorem IsLowerSet.top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsLowerSet s) :

⊤ ∈ s ↔ s = Set.univ

theorem IsUpperSet.top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) :

⊤ ∈ s ↔ Set.Nonempty s

theorem IsUpperSet.not_top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) :

¬⊤ ∈ s ↔ s = ∅

theorem IsUpperSet.bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsUpperSet s) :

⊥ ∈ s ↔ s = Set.univ

theorem IsLowerSet.bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :

⊥ ∈ s ↔ Set.Nonempty s

theorem IsLowerSet.not_bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :

¬⊥ ∈ s ↔ s = ∅

theorem IsUpperSet.not_bddAbove {α : Type u_1} [Preorder α] {s : Set α} [NoMaxOrder α] (hs : IsUpperSet s) :

Set.Nonempty s → ¬BddAbove s

theorem not_bddAbove_Ici {α : Type u_1} [Preorder α] (a : α) [NoMaxOrder α] :

¬BddAbove (Set.Ici a)

theorem not_bddAbove_Ioi {α : Type u_1} [Preorder α] (a : α) [NoMaxOrder α] :

¬BddAbove (Set.Ioi a)

theorem IsLowerSet.not_bddBelow {α : Type u_1} [Preorder α] {s : Set α} [NoMinOrder α] (hs : IsLowerSet s) :

Set.Nonempty s → ¬BddBelow s

theorem not_bddBelow_Iic {α : Type u_1} [Preorder α] (a : α) [NoMinOrder α] :

¬BddBelow (Set.Iic a)

theorem not_bddBelow_Iio {α : Type u_1} [Preorder α] (a : α) [NoMinOrder α] :

¬BddBelow (Set.Iio a)

theorem isUpperSet_iff_forall_lt {α : Type u_1} [PartialOrder α] {s : Set α} :

IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s

theorem isLowerSet_iff_forall_lt {α : Type u_1} [PartialOrder α] {s : Set α} :

IsLowerSet s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s

theorem isUpperSet_iff_Ioi_subset {α : Type u_1} [PartialOrder α] {s : Set α} :

IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Ioi a ⊆ s

theorem isLowerSet_iff_Iio_subset {α : Type u_1} [PartialOrder α] {s : Set α} :

IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Iio a ⊆ s

theorem IsUpperSet.Ioi_subset {α : Type u_1} [PartialOrder α] {s : Set α} :

IsUpperSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Ioi a ⊆ s

Alias of the forward direction of isUpperSet_iff_Ioi_subset.

theorem IsLowerSet.Iio_subset {α : Type u_1} [PartialOrder α] {s : Set α} :

IsLowerSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Iio a ⊆ s

Alias of the forward direction of isLowerSet_iff_Iio_subset.

theorem IsUpperSet.total {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :

s ⊆ t ∨ t ⊆ s

theorem IsLowerSet.total {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :

s ⊆ t ∨ t ⊆ s

Bundled upper/lower sets #

structure UpperSet (α : Type u_6) [LE α] :

Type u_6

carrier : Set α
The carrier of an UpperSet.
upper' : IsUpperSet s.carrier
The carrier of an UpperSet is an upper set.

The type of upper sets of an order.

Instances For

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

Type u_6

carrier : Set α
The carrier of a LowerSet.
lower' : IsLowerSet s.carrier
The carrier of a LowerSet is a lower set.

The type of lower sets of an order.

Instances For

instance UpperSet.instSetLikeUpperSet {α : Type u_1} [LE α] :

SetLike (UpperSet α) α

Equations

UpperSet.instSetLikeUpperSet = { coe := UpperSet.carrier, coe_injective' := (_ : ∀ (s t : UpperSet α), s.carrier = t.carrier → s = t) }

theorem UpperSet.ext {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :

↑s = ↑t → s = t

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

Set α

See Note [custom simps projection].

Equations

UpperSet.Simps.coe s = ↑s

Instances For

@[simp]

theorem UpperSet.carrier_eq_coe {α : Type u_1} [LE α] (s : UpperSet α) :

s.carrier = ↑s

theorem UpperSet.upper {α : Type u_1} [LE α] (s : UpperSet α) :

IsUpperSet ↑s

@[simp]

theorem UpperSet.mem_mk {α : Type u_1} [LE α] (carrier : Set α) (upper' : IsUpperSet carrier) {a : α} :

a ∈ { carrier := carrier, upper' := upper' } ↔ a ∈ carrier

instance LowerSet.instSetLikeLowerSet {α : Type u_1} [LE α] :

SetLike (LowerSet α) α

Equations

LowerSet.instSetLikeLowerSet = { coe := LowerSet.carrier, coe_injective' := (_ : ∀ (s t : LowerSet α), s.carrier = t.carrier → s = t) }

def LowerSet.Simps.coe {α : Type u_1} [LE α] (s : LowerSet α) :

Set α

See Note [custom simps projection].

Equations

LowerSet.Simps.coe s = ↑s

Instances For

theorem LowerSet.ext {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :

↑s = ↑t → s = t

@[simp]

theorem LowerSet.carrier_eq_coe {α : Type u_1} [LE α] (s : LowerSet α) :

s.carrier = ↑s

theorem LowerSet.lower {α : Type u_1} [LE α] (s : LowerSet α) :

IsLowerSet ↑s

@[simp]

theorem LowerSet.mem_mk {α : Type u_1} [LE α] (carrier : Set α) (lower' : IsLowerSet carrier) {a : α} :

a ∈ { carrier := carrier, lower' := lower' } ↔ a ∈ carrier

Order #

instance UpperSet.instSupUpperSet {α : Type u_1} [LE α] :

Sup (UpperSet α)

Equations

UpperSet.instSupUpperSet = { sup := fun s t => { carrier := ↑s ∩ ↑t, upper' := (_ : IsUpperSet (↑s ∩ ↑t)) } }

instance UpperSet.instInfUpperSet {α : Type u_1} [LE α] :

Inf (UpperSet α)

Equations

UpperSet.instInfUpperSet = { inf := fun s t => { carrier := ↑s ∪ ↑t, upper' := (_ : IsUpperSet (↑s ∪ ↑t)) } }

instance UpperSet.instTopUpperSet {α : Type u_1} [LE α] :

Top (UpperSet α)

Equations

UpperSet.instTopUpperSet = { top := { carrier := ∅, upper' := (_ : IsUpperSet ∅) } }

instance UpperSet.instBotUpperSet {α : Type u_1} [LE α] :

Bot (UpperSet α)

Equations

UpperSet.instBotUpperSet = { bot := { carrier := Set.univ, upper' := (_ : IsUpperSet Set.univ) } }

instance UpperSet.instSupSetUpperSet {α : Type u_1} [LE α] :

SupSet (UpperSet α)

Equations

UpperSet.instSupSetUpperSet = { sSup := fun S => { carrier := ⋂ (s : UpperSet α) (_ : s ∈ S), ↑s, upper' := (_ : IsUpperSet (⋂ (i : UpperSet α) (_ : i ∈ S), ↑i)) } }

instance UpperSet.instInfSetUpperSet {α : Type u_1} [LE α] :

InfSet (UpperSet α)

Equations

UpperSet.instInfSetUpperSet = { sInf := fun S => { carrier := ⋃ (s : UpperSet α) (_ : s ∈ S), ↑s, upper' := (_ : IsUpperSet (⋃ (i : UpperSet α) (_ : i ∈ S), ↑i)) } }

instance UpperSet.completelyDistribLattice {α : Type u_1} [LE α] :

CompletelyDistribLattice (UpperSet α)

Equations

One or more equations did not get rendered due to their size.

instance UpperSet.instInhabitedUpperSet {α : Type u_1} [LE α] :

Inhabited (UpperSet α)

Equations

UpperSet.instInhabitedUpperSet = { default := ⊥ }

@[simp]

theorem UpperSet.coe_subset_coe {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :

↑s ⊆ ↑t ↔ t ≤ s

@[simp]

theorem UpperSet.coe_top {α : Type u_1} [LE α] :

↑⊤ = ∅

@[simp]

theorem UpperSet.coe_bot {α : Type u_1} [LE α] :

↑⊥ = Set.univ

@[simp]

theorem UpperSet.coe_eq_univ {α : Type u_1} [LE α] {s : UpperSet α} :

↑s = Set.univ ↔ s = ⊥

@[simp]

theorem UpperSet.coe_eq_empty {α : Type u_1} [LE α] {s : UpperSet α} :

↑s = ∅ ↔ s = ⊤

@[simp]

theorem UpperSet.coe_sup {α : Type u_1} [LE α] (s : UpperSet α) (t : UpperSet α) :

↑(s ⊔ t) = ↑s ∩ ↑t

@[simp]

theorem UpperSet.coe_inf {α : Type u_1} [LE α] (s : UpperSet α) (t : UpperSet α) :

↑(s ⊓ t) = ↑s ∪ ↑t

@[simp]

theorem UpperSet.coe_sSup {α : Type u_1} [LE α] (S : Set (UpperSet α)) :

↑(sSup S) = ⋂ (s : UpperSet α) (_ : s ∈ S), ↑s

@[simp]

theorem UpperSet.coe_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) :

↑(sInf S) = ⋃ (s : UpperSet α) (_ : s ∈ S), ↑s

@[simp]

theorem UpperSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) :

↑(⨆ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

@[simp]

theorem UpperSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) :

↑(⨅ (i : ι), f i) = ⋃ (i : ι), ↑(f i)

theorem UpperSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → UpperSet α) :

↑(⨆ (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 → UpperSet α) :

↑(⨅ (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 : α} :

a ∈ ⊥

@[simp]

theorem UpperSet.mem_sup_iff {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} {a : α} :

a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t

@[simp]

theorem UpperSet.mem_inf_iff {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} {a : α} :

a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem UpperSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} :

a ∈ sSup S ↔ ∀ (s : UpperSet α), s ∈ S → a ∈ s

@[simp]

theorem UpperSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} :

a ∈ sInf S ↔ ∃ s, s ∈ S ∧ a ∈ s

@[simp]

theorem UpperSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → UpperSet α} :

a ∈ ⨆ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

@[simp]

theorem UpperSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → UpperSet α} :

a ∈ ⨅ (i : ι), f i ↔ ∃ i, a ∈ f i

theorem UpperSet.mem_iSup₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → UpperSet α} :

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 → UpperSet α} :

a ∈ ⨅ (i : ι) (j : κ i), f i j ↔ ∃ i j, a ∈ f i j

@[simp]

theorem UpperSet.codisjoint_coe {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :

Codisjoint ↑s ↑t ↔ Disjoint s t

instance LowerSet.instSupLowerSet {α : Type u_1} [LE α] :

Sup (LowerSet α)

Equations

LowerSet.instSupLowerSet = { sup := fun s t => { carrier := ↑s ∪ ↑t, lower' := (_ : ∀ (x x_1 : α), x_1 ≤ x → x ∈ ↑s ∨ x ∈ ↑t → x_1 ∈ ↑s ∨ x_1 ∈ ↑t) } }

instance LowerSet.instInfLowerSet {α : Type u_1} [LE α] :

Inf (LowerSet α)

Equations

LowerSet.instInfLowerSet = { inf := fun s t => { carrier := ↑s ∩ ↑t, lower' := (_ : ∀ (x x_1 : α), x_1 ≤ x → x ∈ ↑s ∧ x ∈ ↑t → x_1 ∈ ↑s ∧ x_1 ∈ ↑t) } }

instance LowerSet.instTopLowerSet {α : Type u_1} [LE α] :

Top (LowerSet α)

Equations

LowerSet.instTopLowerSet = { top := { carrier := Set.univ, lower' := (_ : ∀ (x x_1 : α), x_1 ≤ x → x ∈ Set.univ → x ∈ Set.univ) } }

instance LowerSet.instBotLowerSet {α : Type u_1} [LE α] :

Bot (LowerSet α)

Equations

LowerSet.instBotLowerSet = { bot := { carrier := ∅, lower' := (_ : ∀ (x x_1 : α), x_1 ≤ x → x ∈ ∅ → x ∈ ∅) } }

instance LowerSet.instSupSetLowerSet {α : Type u_1} [LE α] :

SupSet (LowerSet α)

Equations

LowerSet.instSupSetLowerSet = { sSup := fun S => { carrier := ⋃ (s : LowerSet α) (_ : s ∈ S), ↑s, lower' := (_ : IsLowerSet (⋃ (i : LowerSet α) (_ : i ∈ S), ↑i)) } }

instance LowerSet.instInfSetLowerSet {α : Type u_1} [LE α] :

InfSet (LowerSet α)

Equations

LowerSet.instInfSetLowerSet = { sInf := fun S => { carrier := ⋂ (s : LowerSet α) (_ : s ∈ S), ↑s, lower' := (_ : IsLowerSet (⋂ (i : LowerSet α) (_ : i ∈ S), ↑i)) } }

instance LowerSet.completelyDistribLattice {α : Type u_1} [LE α] :

CompletelyDistribLattice (LowerSet α)

Equations

One or more equations did not get rendered due to their size.

instance LowerSet.instInhabitedLowerSet {α : Type u_1} [LE α] :

Inhabited (LowerSet α)

Equations

LowerSet.instInhabitedLowerSet = { default := ⊥ }

theorem LowerSet.coe_subset_coe {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :

↑s ⊆ ↑t ↔ s ≤ t

@[simp]

theorem LowerSet.coe_top {α : Type u_1} [LE α] :

↑⊤ = Set.univ

@[simp]

theorem LowerSet.coe_bot {α : Type u_1} [LE α] :

↑⊥ = ∅

@[simp]

theorem LowerSet.coe_eq_univ {α : Type u_1} [LE α] {s : LowerSet α} :

↑s = Set.univ ↔ s = ⊤

@[simp]

theorem LowerSet.coe_eq_empty {α : Type u_1} [LE α] {s : LowerSet α} :

↑s = ∅ ↔ s = ⊥

@[simp]

theorem LowerSet.coe_sup {α : Type u_1} [LE α] (s : LowerSet α) (t : LowerSet α) :

↑(s ⊔ t) = ↑s ∪ ↑t

@[simp]

theorem LowerSet.coe_inf {α : Type u_1} [LE α] (s : LowerSet α) (t : LowerSet α) :

↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem LowerSet.coe_sSup {α : Type u_1} [LE α] (S : Set (LowerSet α)) :

↑(sSup S) = ⋃ (s : LowerSet α) (_ : s ∈ S), ↑s

@[simp]

theorem LowerSet.coe_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) :

↑(sInf S) = ⋂ (s : LowerSet α) (_ : s ∈ S), ↑s

@[simp]

theorem LowerSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) :

↑(⨆ (i : ι), f i) = ⋃ (i : ι), ↑(f i)

@[simp]

theorem LowerSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) :

↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

theorem LowerSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → LowerSet α) :

↑(⨆ (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 → LowerSet α) :

↑(⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), ↑(f i j)

@[simp]

theorem LowerSet.mem_top {α : Type u_1} [LE α] {a : α} :

a ∈ ⊤

@[simp]

theorem LowerSet.not_mem_bot {α : Type u_1} [LE α] {a : α} :

¬a ∈ ⊥

@[simp]

theorem LowerSet.mem_sup_iff {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} {a : α} :

a ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem LowerSet.mem_inf_iff {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} {a : α} :

a ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t

@[simp]

theorem LowerSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} :

a ∈ sSup S ↔ ∃ s, s ∈ S ∧ a ∈ s

@[simp]

theorem LowerSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} :

a ∈ sInf S ↔ ∀ (s : LowerSet α), s ∈ S → a ∈ s

@[simp]

theorem LowerSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → LowerSet α} :

a ∈ ⨆ (i : ι), f i ↔ ∃ i, a ∈ f i

@[simp]

theorem LowerSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → LowerSet α} :

a ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

theorem LowerSet.mem_iSup₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → LowerSet α} :

a ∈ ⨆ (i : ι) (j : κ i), f i j ↔ ∃ i j, a ∈ f i j

theorem LowerSet.mem_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → LowerSet α} :

a ∈ ⨅ (i : ι) (j : κ i), f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

@[simp]

theorem LowerSet.disjoint_coe {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :

Disjoint ↑s ↑t ↔ Disjoint s t

Complement #

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

The complement of a lower set as an upper set.

Equations

UpperSet.compl s = { carrier := (↑s)ᶜ, lower' := (_ : IsLowerSet (↑s)ᶜ) }

Instances For

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

The complement of a lower set as an upper set.

Equations

LowerSet.compl s = { carrier := (↑s)ᶜ, upper' := (_ : IsUpperSet (↑s)ᶜ) }

Instances For

@[simp]

theorem UpperSet.coe_compl {α : Type u_1} [LE α] (s : UpperSet α) :

↑(UpperSet.compl s) = (↑s)ᶜ

@[simp]

theorem UpperSet.mem_compl_iff {α : Type u_1} [LE α] {s : UpperSet α} {a : α} :

a ∈ UpperSet.compl s ↔ ¬a ∈ s

@[simp]

theorem UpperSet.compl_compl {α : Type u_1} [LE α] (s : UpperSet α) :

LowerSet.compl (UpperSet.compl s) = s

@[simp]

theorem UpperSet.compl_le_compl {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :

UpperSet.compl s ≤ UpperSet.compl t ↔ s ≤ t

@[simp]

theorem UpperSet.compl_sup {α : Type u_1} [LE α] (s : UpperSet α) (t : UpperSet α) :

UpperSet.compl (s ⊔ t) = UpperSet.compl s ⊔ UpperSet.compl t

@[simp]

theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s : UpperSet α) (t : UpperSet α) :

UpperSet.compl (s ⊓ t) = UpperSet.compl s ⊓ UpperSet.compl t

@[simp]

theorem UpperSet.compl_top {α : Type u_1} [LE α] :

UpperSet.compl ⊤ = ⊤

@[simp]

theorem UpperSet.compl_bot {α : Type u_1} [LE α] :

UpperSet.compl ⊥ = ⊥

@[simp]

theorem UpperSet.compl_sSup {α : Type u_1} [LE α] (S : Set (UpperSet α)) :

UpperSet.compl (sSup S) = ⨆ (s : UpperSet α) (_ : s ∈ S), UpperSet.compl s

@[simp]

theorem UpperSet.compl_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) :

UpperSet.compl (sInf S) = ⨅ (s : UpperSet α) (_ : s ∈ S), UpperSet.compl s

@[simp]

theorem UpperSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) :

UpperSet.compl (⨆ (i : ι), f i) = ⨆ (i : ι), UpperSet.compl (f i)

@[simp]

theorem UpperSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) :

UpperSet.compl (⨅ (i : ι), f i) = ⨅ (i : ι), UpperSet.compl (f i)

theorem UpperSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → UpperSet α) :

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

UpperSet.compl (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), UpperSet.compl (f i j)

@[simp]

theorem LowerSet.coe_compl {α : Type u_1} [LE α] (s : LowerSet α) :

↑(LowerSet.compl s) = (↑s)ᶜ

@[simp]

theorem LowerSet.mem_compl_iff {α : Type u_1} [LE α] {s : LowerSet α} {a : α} :

a ∈ LowerSet.compl s ↔ ¬a ∈ s

@[simp]

theorem LowerSet.compl_compl {α : Type u_1} [LE α] (s : LowerSet α) :

UpperSet.compl (LowerSet.compl s) = s

@[simp]

theorem LowerSet.compl_le_compl {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :

LowerSet.compl s ≤ LowerSet.compl t ↔ s ≤ t

theorem LowerSet.compl_sup {α : Type u_1} [LE α] (s : LowerSet α) (t : LowerSet α) :

LowerSet.compl (s ⊔ t) = LowerSet.compl s ⊔ LowerSet.compl t

theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s : LowerSet α) (t : LowerSet α) :

LowerSet.compl (s ⊓ t) = LowerSet.compl s ⊓ LowerSet.compl t

theorem LowerSet.compl_top {α : Type u_1} [LE α] :

LowerSet.compl ⊤ = ⊤

theorem LowerSet.compl_bot {α : Type u_1} [LE α] :

LowerSet.compl ⊥ = ⊥

theorem LowerSet.compl_sSup {α : Type u_1} [LE α] (S : Set (LowerSet α)) :

LowerSet.compl (sSup S) = ⨆ (s : LowerSet α) (_ : s ∈ S), LowerSet.compl s

theorem LowerSet.compl_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) :

LowerSet.compl (sInf S) = ⨅ (s : LowerSet α) (_ : s ∈ S), LowerSet.compl s

theorem LowerSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) :

LowerSet.compl (⨆ (i : ι), f i) = ⨆ (i : ι), LowerSet.compl (f i)

theorem LowerSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) :

LowerSet.compl (⨅ (i : ι), f i) = ⨅ (i : ι), LowerSet.compl (f i)

@[simp]

theorem LowerSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → LowerSet α) :

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

LowerSet.compl (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), LowerSet.compl (f i j)

@[simp]

theorem upperSetIsoLowerSet_apply {α : Type u_1} [LE α] (s : UpperSet α) :

↑upperSetIsoLowerSet s = UpperSet.compl s

@[simp]

theorem upperSetIsoLowerSet_symm_apply {α : Type u_1} [LE α] (s : LowerSet α) :

↑(RelIso.symm upperSetIsoLowerSet) s = LowerSet.compl s

def upperSetIsoLowerSet {α : Type u_1} [LE α] :

UpperSet α ≃o LowerSet α

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} [LinearOrder α] :

IsTotal (UpperSet α) fun x x_1 => x ≤ x_1

Equations

@UpperSet.isTotal_le = @UpperSet.isTotal_le.proof_1

instance LowerSet.isTotal_le {α : Type u_1} [LinearOrder α] :

IsTotal (LowerSet α) fun x x_1 => x ≤ x_1

Equations

@LowerSet.isTotal_le = @LowerSet.isTotal_le.proof_1

noncomputable instance instCompleteLinearOrderUpperSetToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] :

CompleteLinearOrder (UpperSet α)

Equations

One or more equations did not get rendered due to their size.

noncomputable instance instCompleteLinearOrderLowerSetToLEToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLattice {α : Type u_1} [LinearOrder α] :

CompleteLinearOrder (LowerSet α)

Equations

One or more equations did not get rendered due to their size.

Map #

def UpperSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :

UpperSet α ≃o UpperSet β

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem UpperSet.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :

OrderIso.symm (UpperSet.map f) = UpperSet.map (OrderIso.symm f)

@[simp]

theorem UpperSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α ≃o β} {s : UpperSet α} {b : β} :

b ∈ ↑(UpperSet.map f) s ↔ ↑(OrderIso.symm f) b ∈ s

@[simp]

theorem UpperSet.map_refl {α : Type u_1} [Preorder α] :

UpperSet.map (OrderIso.refl α) = OrderIso.refl (UpperSet α)

@[simp]

theorem UpperSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : UpperSet α} (g : β ≃o γ) (f : α ≃o β) :

↑(UpperSet.map g) (↑(UpperSet.map f) s) = ↑(UpperSet.map (OrderIso.trans f g)) s

@[simp]

theorem UpperSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) :

↑(↑(UpperSet.map f) s) = ↑f '' ↑s

def LowerSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :

LowerSet α ≃o LowerSet β

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

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem LowerSet.symm_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) :

OrderIso.symm (LowerSet.map f) = LowerSet.map (OrderIso.symm f)

@[simp]

theorem LowerSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {f : α ≃o β} {b : β} :

b ∈ ↑(LowerSet.map f) s ↔ ↑(OrderIso.symm f) b ∈ s

@[simp]

theorem LowerSet.map_refl {α : Type u_1} [Preorder α] :

LowerSet.map (OrderIso.refl α) = OrderIso.refl (LowerSet α)

@[simp]

theorem LowerSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : LowerSet α} (g : β ≃o γ) (f : α ≃o β) :

↑(LowerSet.map g) (↑(LowerSet.map f) s) = ↑(LowerSet.map (OrderIso.trans f g)) s

@[simp]

theorem LowerSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) :

↑(↑(LowerSet.map f) s) = ↑f '' ↑s

@[simp]

theorem UpperSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) :

UpperSet.compl (↑(UpperSet.map f) s) = ↑(LowerSet.map f) (UpperSet.compl s)

@[simp]

theorem LowerSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) :

LowerSet.compl (↑(LowerSet.map f) s) = ↑(UpperSet.map f) (LowerSet.compl s)

Principal sets #

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

The smallest upper set containing a given element.

Equations

UpperSet.Ici a = { carrier := Set.Ici a, upper' := (_ : IsUpperSet (Set.Ici a)) }

Instances For

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

The smallest upper set containing a given element.

Equations

UpperSet.Ioi a = { carrier := Set.Ioi a, upper' := (_ : IsUpperSet (Set.Ioi a)) }

Instances For

@[simp]

theorem UpperSet.coe_Ici {α : Type u_1} [Preorder α] (a : α) :

↑(UpperSet.Ici a) = Set.Ici a

@[simp]

theorem UpperSet.coe_Ioi {α : Type u_1} [Preorder α] (a : α) :

↑(UpperSet.Ioi a) = Set.Ioi a

@[simp]

theorem UpperSet.mem_Ici_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :

b ∈ UpperSet.Ici a ↔ a ≤ b

@[simp]

theorem UpperSet.mem_Ioi_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :

b ∈ UpperSet.Ioi a ↔ a < b

@[simp]

theorem UpperSet.map_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :

↑(UpperSet.map f) (UpperSet.Ici a) = UpperSet.Ici (↑f a)

@[simp]

theorem UpperSet.map_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :

↑(UpperSet.map f) (UpperSet.Ioi a) = UpperSet.Ioi (↑f a)

theorem UpperSet.Ici_le_Ioi {α : Type u_1} [Preorder α] (a : α) :

UpperSet.Ici a ≤ UpperSet.Ioi a

@[simp]

theorem UpperSet.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] :

UpperSet.Ioi ⊤ = ⊤

@[simp]

theorem UpperSet.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :

UpperSet.Ici ⊥ = ⊥

@[simp]

theorem UpperSet.Ici_sup {α : Type u_1} [SemilatticeSup α] (a : α) (b : α) :

UpperSet.Ici (a ⊔ b) = UpperSet.Ici a ⊔ UpperSet.Ici b

@[simp]

theorem UpperSet.Ici_sSup {α : Type u_1} [CompleteLattice α] (S : Set α) :

UpperSet.Ici (sSup S) = ⨆ (a : α) (_ : a ∈ S), UpperSet.Ici a

@[simp]

theorem UpperSet.Ici_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) :

UpperSet.Ici (⨆ (i : ι), f i) = ⨆ (i : ι), UpperSet.Ici (f i)

theorem UpperSet.Ici_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [CompleteLattice α] (f : (i : ι) → κ i → α) :

UpperSet.Ici (⨆ (i : ι) (j : κ i), f i j) = ⨆ (i : ι) (j : κ i), UpperSet.Ici (f i j)

def LowerSet.Iic {α : Type u_1} [Preorder α] (a : α) :

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

Equations

LowerSet.Iic a = { carrier := Set.Iic a, lower' := (_ : IsLowerSet (Set.Iic a)) }

Instances For

def LowerSet.Iio {α : Type u_1} [Preorder α] (a : α) :

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

Equations

LowerSet.Iio a = { carrier := Set.Iio a, lower' := (_ : IsLowerSet (Set.Iio a)) }

Instances For

@[simp]

theorem LowerSet.coe_Iic {α : Type u_1} [Preorder α] (a : α) :

↑(LowerSet.Iic a) = Set.Iic a

@[simp]

theorem LowerSet.coe_Iio {α : Type u_1} [Preorder α] (a : α) :

↑(LowerSet.Iio a) = Set.Iio a

@[simp]

theorem LowerSet.mem_Iic_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :

b ∈ LowerSet.Iic a ↔ b ≤ a

@[simp]

theorem LowerSet.mem_Iio_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :

b ∈ LowerSet.Iio a ↔ b < a

@[simp]

theorem LowerSet.map_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :

↑(LowerSet.map f) (LowerSet.Iic a) = LowerSet.Iic (↑f a)

@[simp]

theorem LowerSet.map_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) :

↑(LowerSet.map f) (LowerSet.Iio a) = LowerSet.Iio (↑f a)

theorem LowerSet.Ioi_le_Ici {α : Type u_1} [Preorder α] (a : α) :

Set.Ioi a ≤ Set.Ici a

@[simp]

theorem LowerSet.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] :

LowerSet.Iic ⊤ = ⊤

@[simp]

theorem LowerSet.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] :

LowerSet.Iio ⊥ = ⊥

@[simp]

theorem LowerSet.Iic_inf {α : Type u_1} [SemilatticeInf α] (a : α) (b : α) :

LowerSet.Iic (a ⊓ b) = LowerSet.Iic a ⊓ LowerSet.Iic b

@[simp]

theorem LowerSet.Iic_sInf {α : Type u_1} [CompleteLattice α] (S : Set α) :

LowerSet.Iic (sInf S) = ⨅ (a : α) (_ : a ∈ S), LowerSet.Iic a

@[simp]

theorem LowerSet.Iic_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ι → α) :

LowerSet.Iic (⨅ (i : ι), f i) = ⨅ (i : ι), LowerSet.Iic (f i)

theorem LowerSet.Iic_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [CompleteLattice α] (f : (i : ι) → κ i → α) :

LowerSet.Iic (⨅ (i : ι) (j : κ i), f i j) = ⨅ (i : ι) (j : κ i), LowerSet.Iic (f i j)

def upperClosure {α : Type u_1} [Preorder α] (s : Set α) :

The greatest upper set containing a given set.

Equations

upperClosure s = { carrier := {x | ∃ a, a ∈ s ∧ a ≤ x}, upper' := (_ : ∀ (x x_1 : α), x ≤ x_1 → x ∈ {x | ∃ a, a ∈ s ∧ a ≤ x} → ∃ a, a ∈ s ∧ a ≤ x_1) }

Instances For

def lowerClosure {α : Type u_1} [Preorder α] (s : Set α) :

The least lower set containing a given set.

Equations

lowerClosure s = { carrier := {x | ∃ a, a ∈ s ∧ x ≤ a}, lower' := (_ : ∀ (x x_1 : α), x_1 ≤ x → x ∈ {x | ∃ a, a ∈ s ∧ x ≤ a} → ∃ a, a ∈ s ∧ x_1 ≤ a) }

Instances For

@[simp]

theorem mem_upperClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} :

x ∈ upperClosure s ↔ ∃ a, a ∈ s ∧ a ≤ x

@[simp]

theorem mem_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} :

x ∈ lowerClosure s ↔ ∃ a, a ∈ s ∧ x ≤ a

theorem coe_upperClosure {α : Type u_1} [Preorder α] (s : Set α) :

↑(upperClosure s) = ⋃ (a : α) (_ : a ∈ s), Set.Ici a

theorem coe_lowerClosure {α : Type u_1} [Preorder α] (s : Set α) :

↑(lowerClosure s) = ⋃ (a : α) (_ : a ∈ s), Set.Iic a

instance instDecidablePredMemUpperClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun x => ∃ a, a ∈ s ∧ a ≤ x] :

DecidablePred fun x => x ∈ upperClosure s

Equations

instDecidablePredMemUpperClosure = inst

instance instDecidablePredMemLowerClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun x => ∃ a, a ∈ s ∧ x ≤ a] :

DecidablePred fun x => x ∈ lowerClosure s

Equations

instDecidablePredMemLowerClosure = inst

theorem subset_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :

s ⊆ ↑(upperClosure s)

theorem subset_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

s ⊆ ↑(lowerClosure s)

theorem upperClosure_min {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (h : s ⊆ t) (ht : IsUpperSet t) :

↑(upperClosure s) ⊆ t

theorem lowerClosure_min {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (h : s ⊆ t) (ht : IsLowerSet t) :

↑(lowerClosure s) ⊆ t

theorem IsUpperSet.upperClosure {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) :

↑(upperClosure s) = s

theorem IsLowerSet.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) :

↑(lowerClosure s) = s

@[simp]

theorem UpperSet.upperClosure {α : Type u_1} [Preorder α] (s : UpperSet α) :

upperClosure ↑s = s

@[simp]

theorem LowerSet.lowerClosure {α : Type u_1} [Preorder α] (s : LowerSet α) :

lowerClosure ↑s = s

@[simp]

theorem upperClosure_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (f : α ≃o β) :

upperClosure (↑f '' s) = ↑(UpperSet.map f) (upperClosure s)

@[simp]

theorem lowerClosure_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (f : α ≃o β) :

lowerClosure (↑f '' s) = ↑(LowerSet.map f) (lowerClosure s)

@[simp]

theorem UpperSet.iInf_Ici {α : Type u_1} [Preorder α] (s : Set α) :

⨅ (a : α) (_ : a ∈ s), UpperSet.Ici a = upperClosure s

@[simp]

theorem LowerSet.iSup_Iic {α : Type u_1} [Preorder α] (s : Set α) :

⨆ (a : α) (_ : a ∈ s), LowerSet.Iic a = lowerClosure s

theorem gc_upperClosure_coe {α : Type u_1} [Preorder α] :

GaloisConnection (↑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ↑OrderDual.ofDual)

theorem gc_lowerClosure_coe {α : Type u_1} [Preorder α] :

GaloisConnection lowerClosure SetLike.coe

def giUpperClosureCoe {α : Type u_1} [Preorder α] :

GaloisInsertion (↑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ↑OrderDual.ofDual)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def giLowerClosureCoe {α : Type u_1} [Preorder α] :

GaloisInsertion lowerClosure SetLike.coe

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem upperClosure_anti {α : Type u_1} [Preorder α] :

Antitone upperClosure

theorem lowerClosure_mono {α : Type u_1} [Preorder α] :

Monotone lowerClosure

@[simp]

theorem upperClosure_empty {α : Type u_1} [Preorder α] :

upperClosure ∅ = ⊤

@[simp]

theorem lowerClosure_empty {α : Type u_1} [Preorder α] :

lowerClosure ∅ = ⊥

@[simp]

theorem upperClosure_singleton {α : Type u_1} [Preorder α] (a : α) :

upperClosure {a} = UpperSet.Ici a

@[simp]

theorem lowerClosure_singleton {α : Type u_1} [Preorder α] (a : α) :

lowerClosure {a} = LowerSet.Iic a

@[simp]

theorem upperClosure_univ {α : Type u_1} [Preorder α] :

upperClosure Set.univ = ⊥

@[simp]

theorem lowerClosure_univ {α : Type u_1} [Preorder α] :

lowerClosure Set.univ = ⊤

@[simp]

theorem upperClosure_eq_top_iff {α : Type u_1} [Preorder α] {s : Set α} :

upperClosure s = ⊤ ↔ s = ∅

@[simp]

theorem lowerClosure_eq_bot_iff {α : Type u_1} [Preorder α] {s : Set α} :

lowerClosure s = ⊥ ↔ s = ∅

@[simp]

theorem upperClosure_union {α : Type u_1} [Preorder α] (s : Set α) (t : Set α) :

upperClosure (s ∪ t) = upperClosure s ⊓ upperClosure t

@[simp]

theorem lowerClosure_union {α : Type u_1} [Preorder α] (s : Set α) (t : Set α) :

lowerClosure (s ∪ t) = lowerClosure s ⊔ lowerClosure t

@[simp]

theorem upperClosure_iUnion {α : Type u_1} {ι : Sort u_4} [Preorder α] (f : ι → Set α) :

upperClosure (⋃ (i : ι), f i) = ⨅ (i : ι), upperClosure (f i)

@[simp]

theorem lowerClosure_iUnion {α : Type u_1} {ι : Sort u_4} [Preorder α] (f : ι → Set α) :

lowerClosure (⋃ (i : ι), f i) = ⨆ (i : ι), lowerClosure (f i)

@[simp]

theorem upperClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) :

upperClosure (⋃₀ S) = ⨅ (s : Set α) (_ : s ∈ S), upperClosure s

@[simp]

theorem lowerClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) :

lowerClosure (⋃₀ S) = ⨆ (s : Set α) (_ : s ∈ S), lowerClosure s

theorem Set.OrdConnected.upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} (h : Set.OrdConnected s) :

↑(upperClosure s) ∩ ↑(lowerClosure s) = s

theorem ordConnected_iff_upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

Set.OrdConnected s ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

@[simp]

theorem upperBounds_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

upperBounds ↑(lowerClosure s) = upperBounds s

@[simp]

theorem lowerBounds_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :

lowerBounds ↑(upperClosure s) = lowerBounds s

@[simp]

theorem bddAbove_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} :

BddAbove ↑(lowerClosure s) ↔ BddAbove s

@[simp]

theorem bddBelow_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :

BddBelow ↑(upperClosure s) ↔ BddBelow s

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

BddAbove ↑(lowerClosure s) → BddAbove s

Alias of the forward direction of bddAbove_lowerClosure.

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

BddAbove s → BddAbove ↑(lowerClosure s)

Alias of the reverse direction of bddAbove_lowerClosure.

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

BddBelow s → BddBelow ↑(upperClosure s)

Alias of the reverse direction of bddBelow_upperClosure.

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

BddBelow ↑(upperClosure s) → BddBelow s

Alias of the forward direction of bddBelow_upperClosure.

Product #

theorem IsUpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsUpperSet s) (ht : IsUpperSet t) :

IsUpperSet (s ×ˢ t)

theorem IsLowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : IsLowerSet s) (ht : IsLowerSet t) :

IsLowerSet (s ×ˢ t)

def UpperSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :

UpperSet (α × β)

The product of two upper sets as an upper set.

Equations

UpperSet.prod s t = { carrier := ↑s ×ˢ ↑t, upper' := (_ : IsUpperSet (s.carrier ×ˢ ↑t)) }

Instances For

instance UpperSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :

SProd (UpperSet α) (UpperSet β) (UpperSet (α × β))

Equations

UpperSet.instSProd = { sprod := UpperSet.prod }

@[simp]

theorem UpperSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t : UpperSet β) :

↑(s ×ˢ t) = ↑s ×ˢ ↑t

@[simp]

theorem UpperSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : UpperSet α} {t : UpperSet β} :

x ∈ s ×ˢ t ↔ x.fst ∈ s ∧ x.snd ∈ t

theorem UpperSet.Ici_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :

UpperSet.Ici x = UpperSet.Ici x.fst ×ˢ UpperSet.Ici x.snd

@[simp]

theorem UpperSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :

UpperSet.Ici a ×ˢ UpperSet.Ici b = UpperSet.Ici (a, b)

@[simp]

theorem UpperSet.prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) :

s ×ˢ ⊤ = ⊤

@[simp]

theorem UpperSet.top_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : UpperSet β) :

⊤ ×ˢ t = ⊤

@[simp]

theorem UpperSet.bot_prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :

⊥ ×ˢ ⊥ = ⊥

@[simp]

theorem UpperSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : UpperSet α) (s₂ : UpperSet α) (t : UpperSet β) :

(s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t

@[simp]

theorem UpperSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ : UpperSet β) (t₂ : UpperSet β) :

s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂

@[simp]

theorem UpperSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : UpperSet α) (s₂ : UpperSet α) (t : UpperSet β) :

(s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t

@[simp]

theorem UpperSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : UpperSet α) (t₁ : UpperSet β) (t₂ : UpperSet β) :

s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂

theorem UpperSet.prod_sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : UpperSet α) (s₂ : UpperSet α) (t₁ : UpperSet β) (t₂ : UpperSet β) :

s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂)

theorem UpperSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :

s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂

theorem UpperSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t : UpperSet β} :

s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t

theorem UpperSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :

t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂

@[simp]

theorem UpperSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ : UpperSet α} {s₂ : UpperSet α} :

s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂

@[simp]

theorem UpperSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ : UpperSet α} {s₂ : UpperSet α} :

s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂

theorem UpperSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :

s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤

@[simp]

theorem UpperSet.prod_eq_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : UpperSet α} {t : UpperSet β} :

s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤

@[simp]

theorem UpperSet.codisjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : UpperSet α} {s₂ : UpperSet α} {t₁ : UpperSet β} {t₂ : UpperSet β} :

Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂

def LowerSet.prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :

LowerSet (α × β)

The product of two lower sets as a lower set.

Equations

LowerSet.prod s t = { carrier := ↑s ×ˢ ↑t, lower' := (_ : IsLowerSet (s.carrier ×ˢ ↑t)) }

Instances For

instance LowerSet.instSProd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :

SProd (LowerSet α) (LowerSet β) (LowerSet (α × β))

Equations

LowerSet.instSProd = { sprod := LowerSet.prod }

@[simp]

theorem LowerSet.coe_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t : LowerSet β) :

↑(s ×ˢ t) = ↑s ×ˢ ↑t

@[simp]

theorem LowerSet.mem_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} {s : LowerSet α} {t : LowerSet β} :

x ∈ s ×ˢ t ↔ x.fst ∈ s ∧ x.snd ∈ t

theorem LowerSet.Iic_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (x : α × β) :

LowerSet.Iic x = LowerSet.Iic x.fst ×ˢ LowerSet.Iic x.snd

@[simp]

theorem LowerSet.Ici_prod_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) :

LowerSet.Iic a ×ˢ LowerSet.Iic b = LowerSet.Iic (a, b)

@[simp]

theorem LowerSet.prod_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) :

s ×ˢ ⊥ = ⊥

@[simp]

theorem LowerSet.bot_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (t : LowerSet β) :

⊥ ×ˢ t = ⊥

@[simp]

theorem LowerSet.top_prod_top {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :

⊤ ×ˢ ⊤ = ⊤

@[simp]

theorem LowerSet.inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : LowerSet α) (s₂ : LowerSet α) (t : LowerSet β) :

(s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t

@[simp]

theorem LowerSet.prod_inf {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ : LowerSet β) (t₂ : LowerSet β) :

s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂

@[simp]

theorem LowerSet.sup_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : LowerSet α) (s₂ : LowerSet α) (t : LowerSet β) :

(s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t

@[simp]

theorem LowerSet.prod_sup {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : LowerSet α) (t₁ : LowerSet β) (t₂ : LowerSet β) :

s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂

theorem LowerSet.prod_inf_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s₁ : LowerSet α) (s₂ : LowerSet α) (t₁ : LowerSet β) (t₂ : LowerSet β) :

s₁ ×ˢ t₁ ⊓ s₂ ×ˢ t₂ = (s₁ ⊓ s₂) ×ˢ (t₁ ⊓ t₂)

theorem LowerSet.prod_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :

s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂

theorem LowerSet.prod_mono_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t : LowerSet β} :

s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t

theorem LowerSet.prod_mono_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :

t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂

@[simp]

theorem LowerSet.prod_self_le_prod_self {α : Type u_1} [Preorder α] {s₁ : LowerSet α} {s₂ : LowerSet α} :

s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂

@[simp]

theorem LowerSet.prod_self_lt_prod_self {α : Type u_1} [Preorder α] {s₁ : LowerSet α} {s₂ : LowerSet α} :

s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂

theorem LowerSet.prod_le_prod_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :

s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥

@[simp]

theorem LowerSet.prod_eq_bot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {t : LowerSet β} :

s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

@[simp]

theorem LowerSet.disjoint_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s₁ : LowerSet α} {s₂ : LowerSet α} {t₁ : LowerSet β} {t₂ : LowerSet β} :

Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

@[simp]

theorem upperClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) :

upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t