[[!redirects rational closed intervals]] ## Definitions ## ### Large Dedekind real closed intervals ### The **$\mathcal{U}$-large Dedekind real [[closed interval]]s** for a [[universe]] $\mathcal{U}$ is defined as the type of $\mathcal{U}$-[[interval cut]]s on the [[rational numbers]] $\mathbb{Q}$ in a universe: $\mathbb{R}_\mathcal{U} \coloneqq IntervalCut_\mathcal{U}(\mathbb{Q})$. ### Sigma-Dedekind real closed intervals ### The **$\Sigma$-Dedekind real [[closed interval]]s** for a [[sigma-frame|$\sigma$-frame]] $\Sigma$ is defined as the type of $\Sigma$-[[interval cut]]s on the [[rational numbers]] $\mathbb{Q}$: $\mathbb{R}_\Sigma \coloneqq IntervalCut_\Sigma(\mathbb{Q})$. ## See also ## * [[closed interval]] * [[real numbers]] * [[interval cut]]s * [[Dedekind real numbers]] * [[Dedekind cut structure real numbers]] * [[Dedekind real numbers (disambiguation)]]