noncomputable def distToNearestInt (x : ℝ) : ℝ

The distance from a real number to the nearest integer.

Equations

• distToNearestInt x = |x - ↑(round x)|