Up-sets and down-sets

This file proves results on the upper and lower sets in an order.

Main declarations

• upperClosure: The greatest upper set containing a set.
• lowerClosure: The least lower set containing a set.
• UpperSet.Ici: Principal upper set. Set.Ici as an upper set.
• UpperSet.Ioi: Strict principal upper set. Set.Ioi as an upper set.
• LowerSet.Iic: Principal lower set. Set.Iic as a lower set.
• LowerSet.Iio: Strict principal lower set. Set.Iio as a lower set.

Notation

• ×ˢ is notation for UpperSet.prod / LowerSet.prod.

Notes

Upper sets are ordered by reverse inclusion. This convention is motivated by the fact that this makes them order-isomorphic to lower sets and antichains, and matches the convention on Filter.

TODO

Lattice structure on antichains. Order equivalence between upper/lower sets and antichains.

Unbundled upper/lower sets

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

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

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

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

The complement of a lower set as an upper set.

Equations

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

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

The complement of a lower set as an upper set.

Equations

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

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

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

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

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.

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

@[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 : α) : UpperSet α

The smallest upper set containing a given element.

Equations

• UpperSet.Ici a = { carrier := Set.Ici a, upper' := ⋯ }

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

The smallest upper set containing a given element.

Equations

• UpperSet.Ioi a = { carrier := Set.Ioi a, upper' := ⋯ }

@[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 : α) : LowerSet α

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

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

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

Equations

• LowerSet.Iio a = { carrier := Set.Iio a, lower' := ⋯ }

@[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 α) : UpperSet α

The greatest upper set containing a given set.

Equations

• upperClosure s = { carrier := {x : α | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }

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

The least lower set containing a given set.

Equations

• lowerClosure s = { carrier := {x : α | ∃ a ∈ s, x ≤ a}, lower' := ⋯ }

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

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

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.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : BddAbove s → BddAbove ↑(lowerClosure s)

Alias of the reverse direction of bddAbove_lowerClosure.

theorem BddAbove.of_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : BddAbove ↑(lowerClosure s) → BddAbove s

Alias of the forward 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

@[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 α) : LowerSet α

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

Equations

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

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

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

Equations

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

@[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 α) : UpperSet α

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

Equations

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

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

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

Equations

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

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

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

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

@[simp]

theorem lowerClosure_prod {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (s : Set α) (t : Set β) : lowerClosure (s ×ˢ t) = lowerClosure s ×ˢ lowerClosure t