## Dedekind real numbers ## The Dedekind real numbers for a universe $\mathcal{U}$ is defined as the type of [[Dedekind cut]]s on the [[rational numbers]] $\mathbb{Q}$ in a universe: $\mathbb{R}_\mathcal{U} \coloneqq DedekindCut_\mathcal{U}(\mathbb{Q})$ ## See also ## * [[real numbers]] * [[Dedekind cut]]s * [[Dedekind real numbers (disambiguation)]]