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 DirSupClosed {α : Type u_1} [Preorder α] (s : Set α) : Prop

A set s is said to be closed under directed joins if, whenever a directed set d has a least upper bound a and is a subset of s then a also lies in s.

Equations

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

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

A set s is said to be inaccessible by directed joins on D if, when the least upper bound of a directed set d in D lies in s then d has non-empty intersection with s.

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 DirSupInacc {α : Type u_1} [Preorder α] (s : Set α) : Prop

A set s is said to be inaccessible by directed joins if, when the least upper bound of a directed set d lies in s then d has non-empty intersection with s.

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 dirSupInaccOn_univ {α : Type u_1} [Preorder α] {s : Set α} : DirSupInaccOn Set.univ s ↔ DirSupInacc s

@[simp]

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

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of dirSupInacc_compl.

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

Alias of the forward direction of dirSupInacc_compl.

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

Alias of the forward direction of dirSupClosed_compl.

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

Alias of the reverse direction of dirSupClosed_compl.

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

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

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

theorem IsLowerSet.dirSupInacc {α : Type u_1} [Preorder α] {s : Set α} (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.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → d ⊆ s → 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