Documentation

Mathlib.Order.UpperLower.Basic

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 #

theorem isUpperSet_empty {α : Type u_1} [LE α] :
theorem isLowerSet_empty {α : Type u_1} [LE α] :
theorem IsUpperSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : IsUpperSet s) :
theorem IsLowerSet.compl {α : Type u_1} [LE α] {s : Set α} (hs : IsLowerSet s) :
@[simp]
theorem isUpperSet_compl {α : Type u_1} [LE α] {s : Set α} :
@[simp]
theorem isLowerSet_compl {α : Type u_1} [LE α] {s : Set α} :
theorem IsUpperSet.union {α : Type u_1} [LE α] {s t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :
theorem IsLowerSet.union {α : Type u_1} [LE α] {s t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :
theorem IsUpperSet.inter {α : Type u_1} [LE α] {s t : Set α} (hs : IsUpperSet s) (ht : IsUpperSet t) :
theorem IsLowerSet.inter {α : Type u_1} [LE α] {s t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) :
theorem isUpperSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, IsUpperSet s) :
theorem isLowerSet_sUnion {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, 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 : ι) → κ iSet α} (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 : ι) → κ iSet α} (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 : sS, IsUpperSet s) :
theorem isLowerSet_sInter {α : Type u_1} [LE α] {S : Set (Set α)} (hf : sS, 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 : ι) → κ iSet α} (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 : ι) → κ iSet α} (hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)) :
IsLowerSet (⋂ (i : ι), ⋂ (j : κ i), f i j)
theorem IsUpperSet.toDual {α : Type u_1} [LE α] {s : Set α} :

Alias of the reverse direction of isLowerSet_preimage_ofDual_iff.

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

Alias of the reverse direction of isUpperSet_preimage_ofDual_iff.

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

Alias of the reverse direction of isLowerSet_preimage_toDual_iff.

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

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) bs, ct, b cb t
theorem IsLowerSet.isUpperSet_preimage_coe {α : Type u_1} [LE α] {s t : Set α} (hs : IsLowerSet s) :
IsUpperSet (Subtype.val ⁻¹' t) bs, ct, c bb t
theorem IsUpperSet.sdiff {α : Type u_1} [LE α] {s t : Set α} (hs : IsUpperSet s) (ht : bs, ct, b cb t) :
theorem IsLowerSet.sdiff {α : Type u_1} [LE α] {s t : Set α} (hs : IsLowerSet s) (ht : bs, ct, c bb t) :
theorem IsUpperSet.sdiff_of_isLowerSet {α : Type u_1} [LE α] {s t : Set α} (hs : IsUpperSet s) (ht : IsLowerSet t) :
theorem IsLowerSet.sdiff_of_isUpperSet {α : Type u_1} [LE α] {s t : Set α} (hs : IsLowerSet s) (ht : IsUpperSet t) :
theorem IsUpperSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : IsUpperSet s) (has : bs, b ab = a) :
theorem IsLowerSet.erase {α : Type u_1} [LE α] {s : Set α} {a : α} (hs : IsLowerSet s) (has : bs, a bb = a) :
theorem isUpperSet_Ici {α : Type u_1} [Preorder α] (a : α) :
theorem isLowerSet_Iic {α : Type u_1} [Preorder α] (a : α) :
theorem isUpperSet_Ioi {α : Type u_1} [Preorder α] (a : α) :
theorem isLowerSet_Iio {α : Type u_1} [Preorder α] (a : α) :
theorem isUpperSet_iff_Ici_subset {α : Type u_1} [Preorder α] {s : Set α} :
IsUpperSet s ∀ ⦃a : α⦄, a sSet.Ici a s
theorem isLowerSet_iff_Iic_subset {α : Type u_1} [Preorder α] {s : Set α} :
IsLowerSet s ∀ ⦃a : α⦄, a sSet.Iic a s
theorem IsUpperSet.Ici_subset {α : Type u_1} [Preorder α] {s : Set α} :
IsUpperSet s∀ ⦃a : α⦄, a sSet.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 sSet.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) :
theorem IsLowerSet.Iio_subset {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) a : α (ha : a s) :
theorem IsUpperSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) :
theorem IsLowerSet.ordConnected {α : Type u_1} [Preorder α] {s : Set α} (h : IsLowerSet s) :
theorem IsUpperSet.preimage {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsUpperSet s) {f : βα} (hf : Monotone f) :
theorem IsLowerSet.preimage {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} (hs : IsLowerSet s) {f : βα} (hf : Monotone f) :
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} :
@[simp]
theorem isLowerSet_setOf {α : Type u_1} [Preorder α] {p : αProp} :
theorem IsUpperSet.upperBounds_subset {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) :
theorem IsLowerSet.lowerBounds_subset {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) :
theorem IsLowerSet.top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsLowerSet s) :
theorem IsUpperSet.top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) :
theorem IsUpperSet.not_top_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderTop α] (hs : IsUpperSet s) :
s s =
theorem IsUpperSet.bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsUpperSet s) :
theorem IsLowerSet.bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :
theorem IsLowerSet.not_bot_mem {α : Type u_1} [Preorder α] {s : Set α} [OrderBot α] (hs : IsLowerSet s) :
s s =
theorem IsUpperSet.not_bddAbove {α : Type u_1} [Preorder α] {s : Set α} [NoMaxOrder α] (hs : IsUpperSet s) :
theorem not_bddAbove_Ici {α : Type u_1} [Preorder α] (a : α) [NoMaxOrder α] :
theorem not_bddAbove_Ioi {α : Type u_1} [Preorder α] (a : α) [NoMaxOrder α] :
theorem IsLowerSet.not_bddBelow {α : Type u_1} [Preorder α] {s : Set α} [NoMinOrder α] (hs : IsLowerSet s) :
theorem not_bddBelow_Iic {α : Type u_1} [Preorder α] (a : α) [NoMinOrder α] :
theorem not_bddBelow_Iio {α : Type u_1} [Preorder α] (a : α) [NoMinOrder α] :
theorem isUpperSet_iff_forall_lt {α : Type u_1} [PartialOrder α] {s : Set α} :
IsUpperSet s ∀ ⦃a b : α⦄, a < ba sb s
theorem isLowerSet_iff_forall_lt {α : Type u_1} [PartialOrder α] {s : Set α} :
IsLowerSet s ∀ ⦃a b : α⦄, b < aa sb s
theorem isUpperSet_iff_Ioi_subset {α : Type u_1} [PartialOrder α] {s : Set α} :
IsUpperSet s ∀ ⦃a : α⦄, a sSet.Ioi a s
theorem isLowerSet_iff_Iio_subset {α : Type u_1} [PartialOrder α] {s : Set α} :
IsLowerSet s ∀ ⦃a : α⦄, a sSet.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