ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F12119 on D714: Dedekind cut
Formulation 1
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, c) \in {\preceq} \quad \implies \quad x \in c \right) \end{equation}
(3) \begin{equation} \forall \, c \in C : \exists \, c' \in C : (c, c') \in {\preceq} \end{equation}