The maps $[x]\mapsto [mx]$ on $\mathbb{R}\mathrm{/}\mathbb{Z}$ are $m$-sheeted coverings for $m\ge 1$

Given: The objects, hypotheses, and choice principles stated above.

For the quotient by integer translation, $q:\mathbb{R}\to \mathbb{R}\mathrm{/}\mathbb{Z}$ is a covering map, and every deck transformation is a unique translation $x\mapsto x+n$ with $n\in \mathbb{Z}$. (The quotient $\mathbb{R}\to \mathbb{R}\mathrm{/}\mathbb{Z}$ is a covering with integer translations as deck transformations).

A covering map is a continuous surjection $p:E\to B$ such that every $b\in B$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets $V_j$, called sheets, and each restriction $p{\mathrm{\mid }}_{V_j}:V_j\to U$ is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a $U$ is evenly covered, and $p^{-1}(b)$ is the fibre over $b$. A covering is trivial when it is isomorphic over $B$ to a product projection $B\times F\to B$ with $F$ discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

For a covering $p:E\to B$, the cardinality of $p^{-1}(b)$ is locally constant as a function of $b\in B$. If $B$ is connected, all fibres are equinumerous. (The cardinality of a covering fibre is locally constant and is constant on a connected base).

On the set $\mathbb{N}\times \mathbb{N}$ of pairs of natural numbers, define $(a,b)\sim (c,d)⟺a+d=b+c\mathrm{.}$ This is an equivalence relation (lem-int-equivalence). The integers are the quotient $\mathbb{Z}:=(\mathbb{N}\times \mathbb{N})\mathrm{/}\sim ,$ and we write $[(a,b)]$ for the equivalence class of $(a,b)$. (The integers as equivalence classes of pairs of naturals).

Let $a,b\in \mathbb{Z}$ with $b>0$. Then there exist integers $q$ and $r$ with $a=qb+r$ and $0\le r<b$, and this pair is unique (Division with remainder in $\mathbb{Z}$: for $a\in \mathbb{Z}$ and $b>0$ there are unique $q,r\in \mathbb{Z}$ with $a=qb+r$ and $0\le r<b$).