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]
@[simp]
@[simp]
@[simp]
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)
:
theorem
IsLowerSet.isUpperSet_preimage_coe
{α : Type u_1}
[LE α]
{s t : Set α}
(hs : IsLowerSet s)
:
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_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)
:
theorem
IsLowerSet.Iio_subset
{α : Type u_1}
[Preorder α]
{s : Set α}
(h : IsLowerSet s)
⦃a : α⦄
(ha : 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]
@[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
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.total
{α : Type u_1}
[LinearOrder α]
{s t : Set α}
(hs : IsUpperSet s)
(ht : IsUpperSet t)
:
theorem
IsLowerSet.total
{α : Type u_1}
[LinearOrder α]
{s t : Set α}
(hs : IsLowerSet s)
(ht : IsLowerSet t)
: