English
Definition: DirSupInacc(s) holds if for every nonempty directed d and its lub a, whenever a ∈ s, then d meets s.
Русский
Определение: DirSupInacc(s) означает, что для каждого ненулевого направленного множества d и его lub a, если a ∈ s, то d пересекает s.
LaTeX
$$$\\text{DirSupInacc}(s) := \\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 if, when the least upper bound of a
directed set `d` lies in `s` then `d` has non-empty intersection with `s`. -/
def DirSupInacc (s : Set α) : Prop :=
∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
