Intervals without endpoints ordering #
In any decidable linear order
α, we define the set of elements lying between two elements
Icc (min a b) (max a b).
Icc a b requires the assumption
a ≤ b to be meaningful, which is sometimes inconvenient. The
interval as defined in this file is always the set of things lying between
of the relative order of
For real numbers,
Icc (min a b) (max a b) is the same as
segment ℝ a b.
We use the localized notation
[a, b] for
interval a b. One can open the locale
make the notation available.
interval a b is the set of elements lying between