Return to Question

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 subest $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$?

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$?

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 subest $S \subseteq X$ to be a supremum if

$(x \in X \land 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$?

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 subest $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$?

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

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

While a suprema 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 subest $S \subseteq X$ to be a suprema if

$(x \in X \land 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$?

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 subest $S \subseteq X$ to be a supremum if

$(x \in X \land 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$?