## Definitions ## The **locally $\mathcal{U}$-small Dedekind real numbers** for a [[universe]] $\mathcal{U}$ is defined as the [[Archimedean ordered integral domain]] $\mathbb{R}_\mathcal{U}$ with a strictly monotonic function $i:\mathbb{I}_\mathcal{U} \to \mathbb{R}_\mathcal{U}$ from the locally $\mathcal{U}$-small [[Dedekind real unit interval]] $\mathbb{I}_\mathcal{U}$ to $\mathbb{R}_\mathcal{U}$ such that $i(0) = 0$ and $i(1) = 1$. ## See also ## * [[Dedekind real unit interval]] * [[real numbers]] * [[axiom R-flat]] * [[contractibility of Dedekind real numbers]]