PhyslibAlpha.ProbabilisticTheory.OrderUnit.MonotoneComplete

In a monotone-complete ordered space $E$, for any subset $D \subseteq E$ that is nonempty, bounded above, and directed (meaning for every $a, b \in D$, there exists $c \in D$ such that $a \le c$ and $b \le c$), $\text{directedSup}(D)$ is the least upper bound (supremum) of $D$.

In a monotone-complete ordered space $E$, let $D \subseteq E$ be a nonempty subset that is bounded above and directed. Then the element $\text{directedSup}(D)$ is the least upper bound (supremum) of $D$.

Let $E$ be a monotone-complete ordered space. For any monotone sequence $x: \mathbb{N} \to E$, if the range $\{x_n \mid n \in \mathbb{N}\}$ is bounded above, then there exists an element $a \in E$ that is the least upper bound of the range.

Let $E$ be a monotone-complete ordered space. Given a sequence $x: \mathbb{N} \to E$ that is monotone (i.e., $n \le m \implies x_n \le x_m$) and bounded above, the function $\text{rangeSup}(x, h_x, h_{\text{bdd}})$ returns the supremum (least upper bound) of the range of the sequence, denoted as $\sup_{n \in \mathbb{N}} x_n$.

Let $E$ be a monotone-complete ordered space. For any monotone sequence $x: \mathbb{N} \to E$ (where $n \le m$ implies $x_n \le x_m$) such that its range $\{x_n \mid n \in \mathbb{N}\}$ is bounded above, the element $\text{rangeSup}(x, h_x, h_{\text{bounded}})$ is the least upper bound of the range $\{x_n \mid n \in \mathbb{N}\}$.