Directed set (source code)

= Directed set
{wiki}

A directed set is a nonempty <preorder> in which every finite subset has an upper bound. It provides an index set in which any finite collection of stages has a common later stage.