Definition. Least upper bound [dt-0017]

Let X \subseteq Y be a subset of a poset Y. An element y \in Y is a least upper bound (or lub) for X iff:

  1. It is an upper bound: \forall x \in X.\ x \sqsubseteq y
  2. It is less than any other upper bound: \forall y' \in Y.\ (\forall x \in X. x \sqsubseteq y') \Rightarrow y \sqsubseteq y'
It follows that lubs are unique if they exist. We write the lub of a set X as \bigsqcup X, and usually write x \sqcup y as a shorthand for \bigsqcup \{x,y\}.