Intervals without endpoints ordering #
In any lattice
α, we define
uIcc a b to be
Icc (a ⊓ b) (a ⊔ b), which in a linear order is
the set of elements lying between
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,
uIcc a b is the same as
segment ℝ a b.
Finset α (seen as a hypercube of dimension
uIcc a b is the smallest
subcube containing both
We use the localized notation
[[a, b]] for
uIcc a b. One can open the locale
make the notation available.
uIcc a b is the set of elements lying between
Note that we define it more generally in a lattice as
Set.Icc (a ⊓ b) (a ⊔ b). In a product type,
uIcc corresponds to the bounding box of the two elements.