Properties of unbundled upper/lower sets

This file proves results on IsUpperSet and IsLowerSet, including their interactions with set operations, images, preimages and order duals, and properties that reflect stronger assumptions on the underlying order (such as PartialOrder and LinearOrder).

TODO

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

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 t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∪ t)

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

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

theorem IsLowerSet.inter {α : Type u_1} [LE α] {s 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_3} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsUpperSet (f i)) : IsUpperSet (⋃ (i : ι), f i)

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

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

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

theorem isUpperSet_iInter₂ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [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_3} {κ : ι → Sort u_4} [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 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 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 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 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 t : Set α} (hs : IsUpperSet s) (ht : IsLowerSet t) : IsUpperSet (s \ t)

theorem IsLowerSet.sdiff_of_isUpperSet {α : Type u_1} [LE α] {s 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.top_notMem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) : ⊤ ∉ s ↔ s = ∅

@[deprecated IsUpperSet.top_notMem (since := "2025-05-24")]

theorem IsUpperSet.not_top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) : ⊤ ∉ s ↔ s = ∅

Alias of IsUpperSet.top_notMem.

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.bot_notMem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) : ⊥ ∉ s ↔ s = ∅

@[deprecated IsLowerSet.bot_notMem (since := "2025-05-24")]

theorem IsLowerSet.not_bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) : ⊥ ∉ s ↔ s = ∅

Alias of IsLowerSet.bot_notMem.

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

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

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

theorem IsUpperSet.eq_empty_or_Ici {α : Type u_1} [LinearOrder α] {s : Set α} [WellFoundedLT α] (h : IsUpperSet s) : s = ∅ ∨ ∃ (a : α), s = Set.Ici a

theorem IsLowerSet.eq_empty_or_Iic {α : Type u_1} [LinearOrder α] {s : Set α} [WellFoundedGT α] (h : IsLowerSet s) : s = ∅ ∨ ∃ (a : α), s = Set.Iic a

theorem IsLowerSet.eq_univ_or_Iio {α : Type u_1} [LinearOrder α] {s : Set α} [WellFoundedLT α] (h : IsLowerSet s) : s = Set.univ ∨ ∃ (a : α), s = Set.Iio a

theorem IsUpperSet.eq_univ_or_Ioi {α : Type u_1} [LinearOrder α] {s : Set α} [WellFoundedGT α] (h : IsUpperSet s) : s = Set.univ ∨ ∃ (a : α), s = Set.Ioi a