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.
@[simp]
@[simp]
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
isUpperSet_preimage_ofDual_iff
{α : Type u_1}
[LE α]
{s : Set α}
:
IsUpperSet (⇑OrderDual.ofDual ⁻¹' s) ↔ IsLowerSet s
@[simp]
theorem
isLowerSet_preimage_ofDual_iff
{α : Type u_1}
[LE α]
{s : Set α}
:
IsLowerSet (⇑OrderDual.ofDual ⁻¹' s) ↔ IsUpperSet s
@[simp]
theorem
isUpperSet_preimage_toDual_iff
{α : Type u_1}
[LE α]
{s : Set αᵒᵈ}
:
IsUpperSet (⇑OrderDual.toDual ⁻¹' s) ↔ IsLowerSet s
@[simp]
theorem
isLowerSet_preimage_toDual_iff
{α : Type u_1}
[LE α]
{s : Set αᵒᵈ}
:
IsLowerSet (⇑OrderDual.toDual ⁻¹' s) ↔ IsUpperSet 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)
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)
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_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
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.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)
@[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]
@[simp]
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)
:
theorem
IsUpperSet.bot_mem
{α : Type u_1}
[Preorder α]
{s : Set α}
[OrderBot α]
(hs : IsUpperSet s)
:
theorem
IsUpperSet.top_mem
{α : Type u_1}
[Preorder α]
{s : Set α}
[OrderTop α]
(hs : IsUpperSet s)
:
theorem
IsLowerSet.bot_mem
{α : Type u_1}
[Preorder α]
{s : Set α}
[OrderBot α]
(hs : IsLowerSet s)
:
theorem
IsUpperSet.top_notMem
{α : Type u_1}
[Preorder α]
{s : Set α}
[OrderTop α]
(hs : IsUpperSet s)
:
⊤ ∉ s ↔ s = ∅
theorem
IsLowerSet.bot_notMem
{α : 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
IsLowerSet.not_bddBelow
{α : Type u_1}
[Preorder α]
{s : Set α}
[NoMinOrder α]
(hs : IsLowerSet s)
:
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)
:
theorem
IsUpperSet.eq_univ_or_Ioi
{α : Type u_1}
[LinearOrder α]
{s : Set α}
[WellFoundedGT α]
(h : IsUpperSet s)
: