Math formalizes arithmetic as algebraic structures and operations on those structures. Rounding numbers is a common operation. Is there a commonly-accepted formalization of that operation as well?
E.g., could the rounding of rational numbers to integers be approached as an operation from a group to a sub-group (under addition, in this case)? What property would that function have? Would the same properties hold when rounding from real numbers to integers?