Directed set

Remarks

Example: the set of neighbourhoods of a point $x$ in a topological space, ordered by reverse inclusion ($U \le V$ when $V \subseteq U$), is directed. Check: $x$ has the neighbourhood consisting of the whole space, and for neighbourhoods $U, V$ the set $U \cap V$ is a neighbourhood with $U \le U \cap V$ and $V \le U \cap V$.

Non-example: the set $\set{a, b}$ with the trivial order, where each element is only below itself, fails clause 2, since $a$ and $b$ have no common upper bound.

By induction, every finite subset of a directed set has an upper bound in it. A downward directed set is defined dually, with lower bounds. Some authors, and the Mathlib predicate IsDirected, drop clause 1.