Up-sets and down-sets #

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

s.OrdConnected

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

s.OrdConnected

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

s.Nonempty → upperBounds s ⊆ s

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

s.Nonempty → 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 ↔ s.Nonempty

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 ↔ s.Nonempty

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

s.Nonempty → ¬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) :

s.Nonempty → ¬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

Upper/lower sets and Fibrations #

theorem Relation.Fibration.isLowerSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f) {s : Set α} (hs : IsLowerSet s) :

IsLowerSet (f '' s)

theorem IsLowerSet.image_fibration {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f) {s : Set α} (hs : IsLowerSet s) :

IsLowerSet (f '' s)

Alias of Relation.Fibration.isLowerSet_image.

theorem Relation.fibration_iff_isLowerSet_image_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] :

Relation.Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f ↔ ∀ (x : α), IsLowerSet (f '' Set.Iic x)

theorem Relation.fibration_iff_isLowerSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] :

Relation.Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f ↔ ∀ (s : Set α), IsLowerSet s → IsLowerSet (f '' s)

theorem Relation.fibration_iff_image_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] (hf : Monotone f) :

Relation.Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f ↔ ∀ (x : α), f '' Set.Iic x = Set.Iic (f x)

theorem Relation.Fibration.isUpperSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f) {s : Set α} (hs : IsUpperSet s) :

IsUpperSet (f '' s)

theorem IsUpperSet.image_fibration {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f) {s : Set α} (hs : IsUpperSet s) :

IsUpperSet (f '' s)

Alias of Relation.Fibration.isUpperSet_image.

theorem Relation.fibration_iff_isUpperSet_image_Ici {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] :

Relation.Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f ↔ ∀ (x : α), IsUpperSet (f '' Set.Ici x)

theorem Relation.fibration_iff_isUpperSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] :

Relation.Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f ↔ ∀ (s : Set α), IsUpperSet s → IsUpperSet (f '' s)

theorem Relation.fibration_iff_image_Ici {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] (hf : Monotone f) :

Relation.Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f ↔ ∀ (x : α), f '' Set.Ici x = Set.Ici (f x)

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.

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.

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

Instances For

theorem UpperSet.upper' {α : Type u_6} [LE α] (self : UpperSet α) :

IsUpperSet self.carrier

The carrier of an UpperSet is an upper set.

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

Type u_6

The type of lower sets of an order.

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.

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

Instances For

theorem LowerSet.lower' {α : Type u_6} [LE α] (self : LowerSet α) :

IsLowerSet self.carrier

The carrier of a LowerSet is a lower set.

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

SetLike (UpperSet α) α

Equations

UpperSet.instSetLike = { coe := UpperSet.carrier, coe_injective' := ⋯ }

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_iff {α : Type u_1} [LE α] {s : UpperSet α} {t : UpperSet α} :

s = t ↔ ↑s = ↑t

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.instSetLike {α : Type u_1} [LE α] :

SetLike (LowerSet α) α

Equations

LowerSet.instSetLike = { coe := LowerSet.carrier, coe_injective' := ⋯ }

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_iff {α : Type u_1} [LE α] {s : LowerSet α} {t : LowerSet α} :

s = t ↔ ↑s = ↑t

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.instSup {α : Type u_1} [LE α] :

Sup (UpperSet α)

Equations

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

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

Inf (UpperSet α)

Equations

UpperSet.instInf = { inf := fun (s t : UpperSet α) => { carrier := ↑s ∪ ↑t, upper' := ⋯ } }

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

Top (UpperSet α)

Equations

UpperSet.instTop = { top := { carrier := ∅, upper' := ⋯ } }

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

Bot (UpperSet α)

Equations

UpperSet.instBot = { bot := { carrier := Set.univ, upper' := ⋯ } }

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

SupSet (UpperSet α)

Equations

UpperSet.instSupSet = { sSup := fun (S : Set (UpperSet α)) => { carrier := ⋂ s ∈ S, ↑s, upper' := ⋯ } }

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

InfSet (UpperSet α)

Equations

UpperSet.instInfSet = { sInf := fun (S : Set (UpperSet α)) => { carrier := ⋃ s ∈ S, ↑s, upper' := ⋯ } }

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

CompleteLattice (UpperSet α)

Equations

UpperSet.completeLattice = Function.Injective.completeLattice (⇑OrderDual.toDual ∘ SetLike.coe) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

CompletelyDistribLattice (UpperSet α)

Equations

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

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

Inhabited (UpperSet α)

Equations

UpperSet.instInhabited = { 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 α} :

(↑s).Nonempty ↔ 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.instSup {α : Type u_1} [LE α] :

Sup (LowerSet α)

Equations

LowerSet.instSup = { sup := fun (s t : LowerSet α) => { carrier := ↑s ∪ ↑t, lower' := ⋯ } }

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

Inf (LowerSet α)

Equations

LowerSet.instInf = { inf := fun (s t : LowerSet α) => { carrier := ↑s ∩ ↑t, lower' := ⋯ } }

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

Top (LowerSet α)

Equations

LowerSet.instTop = { top := { carrier := Set.univ, lower' := ⋯ } }

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

Bot (LowerSet α)

Equations

LowerSet.instBot = { bot := { carrier := ∅, lower' := ⋯ } }

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

SupSet (LowerSet α)

Equations

LowerSet.instSupSet = { sSup := fun (S : Set (LowerSet α)) => { carrier := ⋃ s ∈ S, ↑s, lower' := ⋯ } }

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

InfSet (LowerSet α)

Equations

LowerSet.instInfSet = { sInf := fun (S : Set (LowerSet α)) => { carrier := ⋂ s ∈ S, ↑s, lower' := ⋯ } }

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

CompleteLattice (LowerSet α)

Equations

LowerSet.completeLattice = Function.Injective.completeLattice SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

CompletelyDistribLattice (LowerSet α)

Equations

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

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

Inhabited (LowerSet α)

Equations

LowerSet.instInhabited = { 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 α} :

(↑s).Nonempty ↔ 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

s.compl = { carrier := (↑s)ᶜ, lower' := ⋯ }

Instances For

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

The complement of a lower set as an upper set.

Equations

s.compl = { carrier := (↑s)ᶜ, upper' := ⋯ }

Instances For

@[simp]

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

↑s.compl = (↑s)ᶜ

@[simp]

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

a ∈ s.compl ↔ a ∉ s

@[simp]

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

s.compl.compl = s

@[simp]

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

s.compl ≤ t.compl ↔ s ≤ t

@[simp]

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

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

@[simp]

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

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

@[simp]

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

⊤.compl = ⊤

@[simp]

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

⊥.compl = ⊥

@[simp]

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

(sSup S).compl = ⨆ s ∈ S, s.compl

@[simp]

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

(sInf S).compl = ⨅ s ∈ S, s.compl

@[simp]

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

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

@[simp]

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

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

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

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

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

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

@[simp]

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

↑s.compl = (↑s)ᶜ

@[simp]

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

a ∈ s.compl ↔ a ∉ s

@[simp]

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

s.compl.compl = s

@[simp]

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

s.compl ≤ t.compl ↔ s ≤ t

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

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

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

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

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

⊤.compl = ⊤

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

⊥.compl = ⊥

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

(sSup S).compl = ⨆ s ∈ S, s.compl

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

(sInf S).compl = ⨅ s ∈ S, s.compl

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

(RelIso.symm upperSetIsoLowerSet) s = s.compl

@[simp]

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

upperSetIsoLowerSet s = s.compl

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

UpperSet α ≃o LowerSet α

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

Equations

upperSetIsoLowerSet = { toFun := UpperSet.compl, invFun := LowerSet.compl, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

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

IsTotal (UpperSet α) fun (x1 x2 : UpperSet α) => x1 ≤ x2

Equations

⋯ = ⋯

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

IsTotal (LowerSet α) fun (x1 x2 : LowerSet α) => x1 ≤ x2

Equations

⋯ = ⋯

noncomputable instance UpperSet.instLinearOrder {α : Type u_1} [LinearOrder α] :

LinearOrder (UpperSet α)

Equations

UpperSet.instLinearOrder = Lattice.toLinearOrder (UpperSet α)

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

LinearOrder (LowerSet α)

Equations

LowerSet.instLinearOrder = Lattice.toLinearOrder (LowerSet α)

noncomputable instance UpperSet.instCompleteLinearOrder {α : Type u_1} [LinearOrder α] :

CompleteLinearOrder (UpperSet α)

Equations

UpperSet.instCompleteLinearOrder = CompleteLinearOrder.mk ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT

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

CompleteLinearOrder (LowerSet α)

Equations

LowerSet.instCompleteLinearOrder = CompleteLinearOrder.mk ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT

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

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

@[simp]

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

b ∈ (UpperSet.map f) s ↔ f.symm 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 (f.trans 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 β) :

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

@[simp]

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

b ∈ (LowerSet.map f) s ↔ f.symm 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 (f.trans 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.map f) s).compl = (LowerSet.map f) s.compl

@[simp]

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

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

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' := ⋯ }

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' := ⋯ }

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' := ⋯ }

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' := ⋯ }

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' := ⋯ }

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' := ⋯ }

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

giLowerClosureCoe = { choice := fun (s : Set α) (hs : ↑(lowerClosure s) ≤ s) => { carrier := s, lower' := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

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 : s.OrdConnected) :

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

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

s.OrdConnected ↔ ↑(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.

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

@[simp]

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

↑(upperClosure s) = s ↔ IsUpperSet s

@[simp]

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

↑(lowerClosure s) = s ↔ IsLowerSet s

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

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

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

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

Instances For

@[simp]

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

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

@[simp]

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

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

@[simp]

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

s.sdiff {a} = s.erase a

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

s.sdiff t ≤ s

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

s.erase a ≤ s

@[simp]

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

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

@[simp]

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

s.erase a = s ↔ a ∉ s

@[simp]

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

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

@[simp]

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

s.erase a < s ↔ a ∈ s

@[simp]

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

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

@[simp]

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

(s.erase a).erase a = s.erase 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) :

s.sdiff 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 ⊔ s.sdiff t = s

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

s.erase 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 ⊔ s.erase 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

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

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

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

Instances For

@[simp]

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

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

@[simp]

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

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

@[simp]

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

s.sdiff {a} = s.erase a

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

s ≤ s.sdiff t

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

s ≤ s.erase a

@[simp]

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

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

@[simp]

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

s.erase a = s ↔ a ∉ s

@[simp]

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

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

@[simp]

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

s < s.erase a ↔ a ∈ s

@[simp]

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

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

@[simp]

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

(s.erase a).erase a = s.erase 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) :

s.sdiff 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 ⊓ s.sdiff t = s

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

s.erase 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 ⊓ s.erase 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

s.prod t = { carrier := ↑s ×ˢ ↑t, upper' := ⋯ }

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

s.prod t = { carrier := ↑s ×ˢ ↑t, lower' := ⋯ }

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