English
A set s is inaccessible by directed joins: whenever a directed nonempty set d has a least upper bound a in s, then d intersects s.
Русский
Множество s недоступно по направленным объединениям: если направленное ненулевое множество d имеет наибольшую верхнюю грань a в s, то d пересекает s.
LaTeX
$$$\\forall d,\\ d\\neq\\emptyset \\to DirectedOn(\\le) d \\to \\forall a,\\ IsLUB\,d\,a \\to a\\in s \\to (d\\cap s)\\neq\\emptyset$$$
Lean4
/-- 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`. -/
def DirSupInaccOn (D : Set (Set α)) (s : Set α) : Prop :=
∀ ⦃d⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
