NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

definition. directed poset [rosiak2022sheaf, def. 285] [tt-0051]

A directed poset is a poset that is inhabited (nonempty) and for which every finite subset has an upper bound. Explicitly,

  • (directedness) \(\forall x,y \in P, \exists z \in P, x \leq z \land y \leq z\)