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