Intervals without endpoints ordering #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
In a product or pi type,
uIcc a b is the smallest box containing
b. For example,
uIcc (1, -1) (-1, 1) = Icc (-1, -1) (1, 1) is the square of vertices
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.
A sort of triangle inequality.
The open-closed interval with unordered bounds.
- set.uIoc = λ (a b : α), set.Ioc (linear_order.min a b) (linear_order.max a b)