Sets closed under directed suprema

We say that a set s is closed under directed suprema whenever it contains all least upper bounds for nonempty, directed subsets. Conversely, a set s is inaccessible by directed suprema whenever its complement is closed under directed suprema. Equivalently, if the least upper bound of a nonempty directed set t is contained in s, then t and s must have nonempty intersection.

Main definitions

• DirSupClosed: sets closed under directed suprema.
• DirSupInacc: sets inaccessible by directed suprema.

def DirSupClosedOn {α : Type u_1} [Preorder α] (D : Set (Set α)) (s : Set α) : Prop

A predicate for a set which is closed under directed suprema of nonempty sets. This is the complement of a DirSupInaccOn set.

Equations

• DirSupClosedOn D s = ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

def DirSupInaccOn {α : Type u_1} [Preorder α] (D : Set (Set α)) (s : Set α) : Prop

A predicate for a set which is inaccessible by directed suprema of nonempty sets in D. This is the complement of a DirSupClosedOn set.

Equations

• DirSupInaccOn D s = ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

def DirSupClosed {α : Type u_1} [Preorder α] (s : Set α) : Prop

A predicate for a set which is closed under directed suprema of nonempty sets. This is the complement of a DirSupInacc set.

Equations

• DirSupClosed s = ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

def DirSupInacc {α : Type u_1} [Preorder α] (s : Set α) : Prop

A predicate for a set which is inaccessible by directed suprema of nonempty sets. This is the complement of a DirSupClosed set.

Equations

• DirSupInacc s = ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

@[simp]

theorem dirSupClosedOn_univ {α : Type u_1} {s : Set α} [Preorder α] : DirSupClosedOn Set.univ s ↔ DirSupClosed s

@[simp]

theorem dirSupInaccOn_univ {α : Type u_1} {s : Set α} [Preorder α] : DirSupInaccOn Set.univ s ↔ DirSupInacc s

@[simp]

theorem DirSupClosed.dirSupClosedOn {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupClosed s → DirSupClosedOn D s

@[simp]

theorem DirSupInacc.dirSupInaccOn {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupInacc s → DirSupInaccOn D s

theorem DirSupClosedOn.mono {α : Type u_1} {s : Set α} {D₁ D₂ : Set (Set α)} [Preorder α] (hD : D₁ ⊆ D₂) (hf : DirSupClosedOn D₂ s) : DirSupClosedOn D₁ s

theorem DirSupInaccOn.mono {α : Type u_1} {s : Set α} {D₁ D₂ : Set (Set α)} [Preorder α] (hD : D₁ ⊆ D₂) (hf : DirSupInaccOn D₂ s) : DirSupInaccOn D₁ s

@[simp]

theorem dirSupClosedOn_compl {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s

@[simp]

theorem dirSupClosed_compl {α : Type u_1} {s : Set α} [Preorder α] : DirSupClosed sᶜ ↔ DirSupInacc s

@[simp]

theorem dirSupInaccOn_compl {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s

@[simp]

theorem dirSupInacc_compl {α : Type u_1} {s : Set α} [Preorder α] : DirSupInacc sᶜ ↔ DirSupClosed s

theorem DirSupClosedOn.of_compl {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupClosedOn D sᶜ → DirSupInaccOn D s

Alias of the forward direction of dirSupClosedOn_compl.

theorem DirSupInaccOn.compl {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupInaccOn D s → DirSupClosedOn D sᶜ

Alias of the reverse direction of dirSupClosedOn_compl.

theorem DirSupClosedOn.compl {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupClosedOn D s → DirSupInaccOn D sᶜ

Alias of the reverse direction of dirSupInaccOn_compl.

theorem DirSupInaccOn.of_compl {α : Type u_1} {s : Set α} {D : Set (Set α)} [Preorder α] : DirSupInaccOn D sᶜ → DirSupClosedOn D s

Alias of the forward direction of dirSupInaccOn_compl.

theorem DirSupInacc.compl {α : Type u_1} {s : Set α} [Preorder α] : DirSupInacc s → DirSupClosed sᶜ

Alias of the reverse direction of dirSupClosed_compl.

theorem DirSupClosed.of_compl {α : Type u_1} {s : Set α} [Preorder α] : DirSupClosed sᶜ → DirSupInacc s

Alias of the forward direction of dirSupClosed_compl.

theorem DirSupClosed.compl {α : Type u_1} {s : Set α} [Preorder α] : DirSupClosed s → DirSupInacc sᶜ

Alias of the reverse direction of dirSupInacc_compl.

theorem DirSupInacc.of_compl {α : Type u_1} {s : Set α} [Preorder α] : DirSupInacc sᶜ → DirSupClosed s

Alias of the forward direction of dirSupInacc_compl.

@[simp]

theorem DirSupClosed.empty {α : Type u_1} [Preorder α] : DirSupClosed ∅

@[simp]

theorem DirSupInacc.empty {α : Type u_1} [Preorder α] : DirSupInacc ∅

theorem DirSupClosedOn.empty {α : Type u_1} {D : Set (Set α)} [Preorder α] : DirSupClosedOn D ∅

theorem DirSupInaccOn.empty {α : Type u_1} {D : Set (Set α)} [Preorder α] : DirSupInaccOn D ∅

@[simp]

theorem DirSupClosed.univ {α : Type u_1} [Preorder α] : DirSupClosed Set.univ

@[simp]

theorem DirSupInacc.univ {α : Type u_1} [Preorder α] : DirSupInacc Set.univ

theorem DirSupClosedOn.univ {α : Type u_1} {D : Set (Set α)} [Preorder α] : DirSupClosedOn D Set.univ

theorem DirSupInaccOn.univ {α : Type u_1} {D : Set (Set α)} [Preorder α] : DirSupInaccOn D Set.univ

theorem DirSupClosedOn.sInter {α : Type u_1} {D : Set (Set α)} [Preorder α] {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosedOn D x) : DirSupClosedOn D (⋂₀ s)

theorem DirSupClosed.sInter {α : Type u_1} [Preorder α] {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosed x) : DirSupClosed (⋂₀ s)

theorem DirSupInaccOn.sUnion {α : Type u_1} {D : Set (Set α)} [Preorder α] {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInaccOn D x) : DirSupInaccOn D (⋃₀ s)

theorem DirSupInacc.sUnion {α : Type u_1} [Preorder α] {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInacc x) : DirSupInacc (⋃₀ s)

theorem DirSupClosedOn.iInter {α : Type u_1} {D : Set (Set α)} [Preorder α] {ι : Sort u_2} {f : ι → Set α} (hs : ∀ (i : ι), DirSupClosedOn D (f i)) : DirSupClosedOn D (⋂ (i : ι), f i)

theorem DirSupClosed.iInter {α : Type u_1} [Preorder α] {ι : Sort u_2} {f : ι → Set α} (hs : ∀ (i : ι), DirSupClosed (f i)) : DirSupClosed (⋂ (i : ι), f i)

theorem DirSupInaccOn.iUnion {α : Type u_1} {D : Set (Set α)} [Preorder α] {ι : Sort u_2} {f : ι → Set α} (hs : ∀ (i : ι), DirSupInaccOn D (f i)) : DirSupInaccOn D (⋃ (i : ι), f i)

theorem DirSupInacc.iUnion {α : Type u_1} [Preorder α] {ι : Sort u_2} {f : ι → Set α} (hs : ∀ (i : ι), DirSupInacc (f i)) : DirSupInacc (⋃ (i : ι), f i)

theorem DirSupClosedOn.inter {α : Type u_1} {s t : Set α} {D : Set (Set α)} [Preorder α] (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : DirSupClosedOn D (s ∩ t)

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

theorem DirSupInaccOn.union {α : Type u_1} {s t : Set α} {D : Set (Set α)} [Preorder α] (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : DirSupInaccOn D (s ∪ t)

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

theorem IsUpperSet.dirSupClosed {α : Type u_1} {s : Set α} [Preorder α] (hs : IsUpperSet s) : DirSupClosed s

theorem IsLowerSet.dirSupInacc {α : Type u_1} {s : Set α} [Preorder α] (hs : IsLowerSet s) : DirSupInacc s

theorem dirSupClosed_Iic {α : Type u_1} [Preorder α] (a : α) : DirSupClosed (Set.Iic a)

theorem dirSupClosed_iff_forall_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} : DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → sSup d ∈ s

theorem dirSupInacc_iff_forall_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} : DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty