For a poset $X$ we define an upperbound $w \in X$ of a subset $S \subseteq X$ to be a weak-supremum if

$(\forall a \in S (a \leq b)) \implies w \leq b$.

While a supremum is defined more carefully (in terms of an excess relation $\not\leq$ on $X$). That is, we define and upperbound $s \in X$ of an inhabited subset $S \subseteq X$ to be a supremum if

$\forall x \in X(s \not\leq x \implies \exists a \in S (a \not\leq x))$,

This differentiation between suprema primarily comes up in constructive analysis when the poset $X = \mathbb{R}$. But, I am currently studying lattice theory constructively and the question began to arise. Given a poset $X$ and a subset $S \subseteq X$ how do we define the join of $S$, $\bigvee S$?

5more comments