English
The round function on α is defined by rounding to the nearest integer: round(x) is the integer nearest to x, given by floor(x) when 2·fract(x) < 1 and ceil(x) otherwise.
Русский
Функция округления на α определяется как округление к ближайшему целому: round(x) является целым, ближайшим к x, равное floor(x) если 2·fract(x) < 1 и иначе ceil(x).
LaTeX
$$$\operatorname{round}(x) = \begin{cases} \lfloor x \rfloor, & 2\,\operatorname{fract}(x) < 1/1 \\ \lceil x \rceil, & \text{иначе} \end{cases}$$$
Lean4
/-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
def round (x : α) : ℤ :=
if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉
