How to formally define decimal truncation?

Question

Let $n$ be a non-negative integer. How does one formally define a function from reals to reals such that a real number $r$ is correct to $n$ places after the decimal point? So, for example $f_0(\pi)=3$, $f_1(-1.13)=-1.1$, $f_2(0.006666..)=0$ etc. I know intuitively what the function is, I just would like the function to be given a rigorous definition.

Answer 1

$$f_n(r)=10^{-n}\operatorname{sign}(r)\left\lfloor 10^n|r|\right\rfloor$$

Where $\lfloor x\rfloor$ is the greatest integer $\leq x.$

This can be written as:

$$f_n(r)=10^{-n}f_0(10^nr)\tag1$$

The use of absolute values and $\operatorname{sign}$ reflects that it is somewhat arbitrary to “truncate” towards zero.

For example, if $r$ is positive and $n$ is a positive integer, then $f_0(r+n)=f_0(r)+n,$ but this doesn’t generalize to all real $r$ and integers $n.$

You could substitute $$g_{0}(r)=\left\lfloor r+\frac12\right\rfloor$$ and define $g_n$ using the equivalent of (1) to define rounding to $n$ digits.

Rounding is more natural because $g_0(r+n)=g_0(r)+n$ for all real $r$ and integer $n.$ The only time you will get $f_0(-r)\neq -f_0(r)$ is when $r$ is exactly a half-integer.