Thanks.

I realize now. Initially, I was just concerned with different base representations of the real numbers. In this case, I approached binary seriously for the first time, with no regard to its popular place in computer coding (hence "purely mathematical context"). Still, I wondered how rounding would apply and that in itself is more native to application. So my words were rather misplaced.

However, I guess one could still view it in a pure sense. Can't rounding be formalized as...?

Consider the rounding function

where

. For some real number

in base

,

is defined as the number for which

is closest to whose expansion terminates at

.

So

would round

to the nearest hundredth, giving

, because it is the closest number to

whose expansion terminates at

(i.e. rounding to the nearest hundredth).

Sorry if it seems pointless, but one can be curious.