ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Binary endorelation ▼ Preordering relation ▼ Partial ordering relation ▼ Ordering relation ▼ Ordered set
Definition D714
Dedekind cut

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) $$\emptyset \neq C \neq X$$ (2) $$\forall \, x \in X : \forall \, c \in C \left( (x, c) \in {\preceq} \quad \implies \quad x \in c \right)$$ (3) $$\forall \, c \in C : \exists \, c' \in C : (c, c') \in {\preceq}$$

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) $$\emptyset \neq C \neq X$$ (2) $$\forall \, x \in X : \forall \, c \in C \left( x \preceq c \quad \implies \quad x \in c \right)$$ (3) $$\forall \, c \in C : \exists \, c' \in C : c \preceq c'$$
Children
 ▶ Set of real numbers