English
A set s is DirSupClosed if whenever a directed nonempty set d has lub a and d ⊆ s, then a ∈ s.
Русский
Множество s является DirSupClosed, если для любого направленного ненулевого множества d его наибольшая верхняя граница a принадлежит s, когда d ⊆ s.
LaTeX
$$$\\text{DirSupClosed}(s) := \\forall d\\ (d\\neq\\emptyset)\\to DirectedOn(\\le) d \\to \\forall a\\ IsLUB\,d\,a \\to d\\subseteq s \\to a\\in s$$$
Lean4
/-- 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`.
-/
def DirSupClosed (s : Set α) : Prop :=
∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → d ⊆ s → a ∈ s
