**Description: **Define the floor
(greatest integer less than or equal to) function. See
flval 9116 for its value, flqlelt 9118 for its basic property, and flqcl 9117 for
its closure. For example, while
(ex-fl 9895).
Although we define this on real numbers so that notations are similar to
the Metamath Proof Explorer, in the absence of excluded middle few
theorems will be possible beyond the rationals. Imagine a real number
which is around 2.99995 or 3.00001 . In order to determine whether its
floor is 2 or 3, it would be necessary to compute the number to
arbitrary precision.
The term "floor" was coined by Ken Iverson. He also invented
a
mathematical notation for floor, consisting of an L-shaped left bracket
and its reflection as a right bracket. In APL, the left-bracket alone
is used, and we borrow this idea. (Thanks to Paul Chapman for this
information.) (Contributed by NM,
14-Nov-2004.) |