ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F12120 on D714: Dedekind cut
Formulation 2
Let $P = (X, {\preceq})$ be an D1707: Ordered set.
A D11: Set $D \subseteq X$ is a Dedekind cut in $P$ if and only if
(1) \begin{equation} \emptyset \neq C \neq X \end{equation}
(2) \begin{equation} \forall \, x \in X : \forall \, c \in C \left( x \preceq c \quad \implies \quad x \in c \right) \end{equation}
(3) \begin{equation} \forall \, c \in C : \exists \, c' \in C : c \preceq c' \end{equation}