\begin{definition}[Definition:Ceiling Function/Definition 1]
Let $x$ be a real number.
The '''ceiling function of $x$''' is defined as the infimum of the set of integers no smaller than $x$:
:$\ceiling x := \inf \set {m \in \Z: x \le m}$
where $\le$ is the usual ordering on the real numbers.
\end{definition}