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 ∈ S, IsUpperSet s) :

IsUpperSet (⋃₀ S)

theorem isLowerSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ 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 ∈ S, IsUpperSet s) :

IsUpperSet (⋂₀ S)

theorem isLowerSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : ∀ 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.isLowerSet_preimage_coe {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) :

IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

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

IsUpperSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t

theorem IsUpperSet.sdiff {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsUpperSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :

IsUpperSet (s \ t)

theorem IsLowerSet.sdiff {α : Type u_1} [LE α] {s : Set α} {t : Set α} (hs : IsLowerSet s) (ht : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :

IsLowerSet (s \ t)

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

IsUpperSet (s \ t)

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

IsLowerSet (s \ t)

theorem IsUpperSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : IsUpperSet s) (has : ∀ b ∈ s, b ≤ a → b = a) :

IsUpperSet (s \ {a})

theorem IsLowerSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : IsLowerSet s) (has : ∀ b ∈ s, a ≤ b → b = a) :

IsLowerSet (s \ {a})

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.Ioi_subset {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) ⦃a : α⦄ (ha : a ∈ s) :

Set.Ioi a ⊆ s

theorem IsLowerSet.Iio_subset {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) ⦃a : α⦄ (ha : a ∈ s) :

Set.Iio a ⊆ s

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)

theorem OrderEmbedding.image_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsUpperSet (Set.range ⇑e)) (a : α) :

⇑e '' Set.Ici a = Set.Ici (e a)

theorem OrderEmbedding.image_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsLowerSet (Set.range ⇑e)) (a : α) :

⇑e '' Set.Iic a = Set.Iic (e a)

theorem OrderEmbedding.image_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsUpperSet (Set.range ⇑e)) (a : α) :

⇑e '' Set.Ioi a = Set.Ioi (e a)

theorem OrderEmbedding.image_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (he : IsLowerSet (Set.range ⇑e)) (a : α) :

⇑e '' Set.Iio a = Set.Iio (e a)

@[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 IsUpperSet.upperBounds_subset {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) :

Set.Nonempty s → upperBounds s ⊆ s

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

Set.Nonempty s → lowerBounds s ⊆ s

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.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

The type of upper sets of an order.

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

Instances For

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

Type u_6

The type of lower sets of an order.

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

Instances For

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

SetLike (UpperSet α) α

Equations

UpperSet.instSetLikeUpperSet = { coe := UpperSet.carrier, coe_injective' := (_ : ∀ (s t : UpperSet α), s.carrier = t.carrier → 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

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

↑s = ↑t → s = t

@[simp]

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

s.carrier = ↑s

@[simp]

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

IsUpperSet ↑s

@[simp]

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

↑{ carrier := s, upper' := hs } = s

@[simp]

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

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

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

@[simp]

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

IsLowerSet ↑s

@[simp]

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

↑{ carrier := s, lower' := hs } = s

@[simp]

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

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

Order #

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

Sup (UpperSet α)

Equations

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

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

Inf (UpperSet α)

Equations

UpperSet.instInfUpperSet = { inf := fun (s t : UpperSet α) => { 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 : Set (UpperSet α)) => { carrier := ⋂ s ∈ S, ↑s, upper' := (_ : IsUpperSet (⋂ i ∈ S, ↑i)) } }

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

InfSet (UpperSet α)

Equations

UpperSet.instInfSetUpperSet = { sInf := fun (S : Set (UpperSet α)) => { carrier := ⋃ s ∈ S, ↑s, upper' := (_ : IsUpperSet (⋃ 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_ssubset_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_nonempty {α : Type u_1} [LE α] {s : UpperSet α} :

Set.Nonempty ↑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 ∈ S, ↑s

@[simp]

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

↑(sInf S) = ⋃ 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 ∈ S, a ∈ s

@[simp]

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

a ∈ sInf 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 : κ i), 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 : LowerSet α) => { 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 : LowerSet α) => { 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 : Set (LowerSet α)) => { carrier := ⋃ s ∈ S, ↑s, lower' := (_ : IsLowerSet (⋃ i ∈ S, ↑i)) } }

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

InfSet (LowerSet α)

Equations

LowerSet.instInfSetLowerSet = { sInf := fun (S : Set (LowerSet α)) => { carrier := ⋂ s ∈ S, ↑s, lower' := (_ : IsLowerSet (⋂ 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

theorem LowerSet.coe_ssubset_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_nonempty {α : Type u_1} [LE α] {s : LowerSet α} :

Set.Nonempty ↑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 ∈ S, ↑s

@[simp]

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

↑(sInf S) = ⋂ 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, a ∈ s

@[simp]

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

a ∈ sInf S ↔ ∀ 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 : κ i), 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 ∈ S, UpperSet.compl s

@[simp]

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

UpperSet.compl (sInf S) = ⨅ 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 ∈ S, LowerSet.compl s

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

LowerSet.compl (sInf S) = ⨅ 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_symm_apply {α : Type u_1} [LE α] (s : LowerSet α) :

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

@[simp]

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

upperSetIsoLowerSet s = UpperSet.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 : UpperSet α) => x ≤ x_1

Equations

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

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

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

Equations

(_ : IsTotal (LowerSet α) fun (x x_1 : LowerSet α) => x ≤ x_1) = (_ : IsTotal (LowerSet α) fun (x x_1 : LowerSet α) => x ≤ x_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.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] :

UpperSet.Ici ⊥ = ⊥

@[simp]

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

UpperSet.Ioi ⊤ = ⊤

@[simp]

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

UpperSet.Ici a ≠ ⊤

@[simp]

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

UpperSet.Ici a < ⊤

@[simp]

theorem UpperSet.le_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :

s ≤ UpperSet.Ici a ↔ a ∈ s

theorem UpperSet.Ici_injective {α : Type u_1} [PartialOrder α] :

Function.Injective UpperSet.Ici

@[simp]

theorem UpperSet.Ici_inj {α : Type u_1} [PartialOrder α] {a : α} {b : α} :

UpperSet.Ici a = UpperSet.Ici b ↔ a = b

theorem UpperSet.Ici_ne_Ici {α : Type u_1} [PartialOrder α] {a : α} {b : α} :

UpperSet.Ici a ≠ UpperSet.Ici b ↔ a ≠ b

@[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 ∈ 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_ne_bot {α : Type u_1} [Preorder α] {a : α} :

LowerSet.Iic a ≠ ⊥

@[simp]

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

⊥ < LowerSet.Iic a

@[simp]

theorem LowerSet.Iic_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :

LowerSet.Iic a ≤ s ↔ a ∈ s

theorem LowerSet.Iic_injective {α : Type u_1} [PartialOrder α] :

Function.Injective LowerSet.Iic

@[simp]

theorem LowerSet.Iic_inj {α : Type u_1} [PartialOrder α] {a : α} {b : α} :

LowerSet.Iic a = LowerSet.Iic b ↔ a = b

theorem LowerSet.Iic_ne_Iic {α : Type u_1} [PartialOrder α] {a : α} {b : α} :

LowerSet.Iic a ≠ LowerSet.Iic b ↔ a ≠ b

@[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 ∈ 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 ∈ s, a ≤ x}, upper' := (_ : ∀ (x x_1 : α), x ≤ x_1 → x ∈ {x : α | ∃ a ∈ s, a ≤ x} → ∃ 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 ∈ s, x ≤ a}, lower' := (_ : ∀ (x x_1 : α), x_1 ≤ x → x ∈ {x : α | ∃ a ∈ s, x ≤ a} → ∃ a ∈ s, x_1 ≤ a) }

Instances For

@[simp]

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

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

@[simp]

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

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

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

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

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

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

instance instDecidablePredMemUpperClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun (x : α) => ∃ 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 ∈ 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 ∈ s, UpperSet.Ici a = upperClosure s

@[simp]

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

⨆ a ∈ s, LowerSet.Iic a = lowerClosure s

@[simp]

theorem lowerClosure_le {α : Type u_1} [Preorder α] {s : Set α} {t : LowerSet α} :

lowerClosure s ≤ t ↔ s ⊆ ↑t

@[simp]

theorem le_upperClosure {α : Type u_1} [Preorder α] {t : Set α} {s : UpperSet α} :

s ≤ upperClosure t ↔ t ⊆ ↑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 ∈ S, upperClosure s

@[simp]

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

lowerClosure (⋃₀ S) = ⨆ 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.of_upperClosure {α : Type u_1} [Preorder α] {s : Set α} :

BddBelow ↑(upperClosure s) → BddBelow s

Alias of the forward direction of bddBelow_upperClosure.

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

BddBelow s → BddBelow ↑(upperClosure s)

Alias of the reverse direction of bddBelow_upperClosure.

@[simp]

theorem IsLowerSet.disjoint_upperClosure_left {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (ht : IsLowerSet t) :

Disjoint (↑(upperClosure s)) t ↔ Disjoint s t

@[simp]

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

Disjoint s ↑(upperClosure t) ↔ Disjoint s t

@[simp]

theorem IsUpperSet.disjoint_lowerClosure_left {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (ht : IsUpperSet t) :

Disjoint (↑(lowerClosure s)) t ↔ Disjoint s t

@[simp]

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

Disjoint s ↑(lowerClosure t) ↔ Disjoint s t

Set Difference #

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

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

Equations

LowerSet.sdiff s t = { carrier := ↑s \ ↑(upperClosure t), lower' := (_ : IsLowerSet (↑s \ ↑(upperClosure t))) }

Instances For

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

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

Equations

LowerSet.erase s a = { carrier := ↑s \ ↑(UpperSet.Ici a), lower' := (_ : IsLowerSet (↑s \ ↑(UpperSet.Ici a))) }

Instances For

@[simp]

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

↑(LowerSet.sdiff s t) = ↑s \ ↑(upperClosure t)

@[simp]

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

↑(LowerSet.erase s a) = ↑s \ ↑(UpperSet.Ici a)

@[simp]

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

LowerSet.sdiff s {a} = LowerSet.erase s a

theorem LowerSet.sdiff_le_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} :

LowerSet.sdiff s t ≤ s

theorem LowerSet.erase_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :

LowerSet.erase s a ≤ s

@[simp]

theorem LowerSet.sdiff_eq_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} :

LowerSet.sdiff s t = s ↔ Disjoint (↑s) t

@[simp]

theorem LowerSet.erase_eq {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :

LowerSet.erase s a = s ↔ a ∉ s

@[simp]

theorem LowerSet.sdiff_lt_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} :

LowerSet.sdiff s t < s ↔ ¬Disjoint (↑s) t

@[simp]

theorem LowerSet.erase_lt {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} :

LowerSet.erase s a < s ↔ a ∈ s

@[simp]

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

LowerSet.sdiff (LowerSet.sdiff s t) t = LowerSet.sdiff s t

@[simp]

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

LowerSet.erase (LowerSet.erase s a) a = LowerSet.erase s a

theorem LowerSet.sdiff_sup_lowerClosure {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :

LowerSet.sdiff s t ⊔ lowerClosure t = s

theorem LowerSet.lowerClosure_sup_sdiff {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :

lowerClosure t ⊔ LowerSet.sdiff s t = s

theorem LowerSet.erase_sup_Iic {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) :

LowerSet.erase s a ⊔ LowerSet.Iic a = s

theorem LowerSet.Iic_sup_erase {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) :

LowerSet.Iic a ⊔ LowerSet.erase s a = s

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

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

Equations

UpperSet.sdiff s t = { carrier := ↑s \ ↑(lowerClosure t), upper' := (_ : IsUpperSet (↑s \ ↑(lowerClosure t))) }

Instances For

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

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

Equations

UpperSet.erase s a = { carrier := ↑s \ ↑(LowerSet.Iic a), upper' := (_ : IsUpperSet (↑s \ ↑(LowerSet.Iic a))) }

Instances For

@[simp]

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

↑(UpperSet.sdiff s t) = ↑s \ ↑(lowerClosure t)

@[simp]

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

↑(UpperSet.erase s a) = ↑s \ ↑(LowerSet.Iic a)

@[simp]

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

UpperSet.sdiff s {a} = UpperSet.erase s a

theorem UpperSet.le_sdiff_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} :

s ≤ UpperSet.sdiff s t

theorem UpperSet.le_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :

s ≤ UpperSet.erase s a

@[simp]

theorem UpperSet.sdiff_eq_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} :

UpperSet.sdiff s t = s ↔ Disjoint (↑s) t

@[simp]

theorem UpperSet.erase_eq {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :

UpperSet.erase s a = s ↔ a ∉ s

@[simp]

theorem UpperSet.lt_sdiff_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} :

s < UpperSet.sdiff s t ↔ ¬Disjoint (↑s) t

@[simp]

theorem UpperSet.lt_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} :

s < UpperSet.erase s a ↔ a ∈ s

@[simp]

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

UpperSet.sdiff (UpperSet.sdiff s t) t = UpperSet.sdiff s t

@[simp]

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

UpperSet.erase (UpperSet.erase s a) a = UpperSet.erase s a

theorem UpperSet.sdiff_inf_upperClosure {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :

UpperSet.sdiff s t ⊓ upperClosure t = s

theorem UpperSet.upperClosure_inf_sdiff {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :

upperClosure t ⊓ UpperSet.sdiff s t = s

theorem UpperSet.erase_inf_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) :

UpperSet.erase s a ⊓ UpperSet.Ici a = s

theorem UpperSet.Ici_inf_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) :

UpperSet.Ici a ⊓ UpperSet.erase s a = s

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.1 ∈ s ∧ x.2 ∈ t

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

UpperSet.Ici x = UpperSet.Ici x.1 ×ˢ UpperSet.Ici x.2

@[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.1 ∈ s ∧ x.2 ∈ t

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

LowerSet.Iic x = LowerSet.Iic x.1 ×ˢ LowerSet.Iic x.2

@[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