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.
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, b]] denotes the set of elements lying between
- One or more equations did not get rendered due to their size.
A sort of triangle inequality.
Ι a b denotes the open-closed interval with unordered bounds. Here,
Ι is a capital iota,
distinguished from a capital
- Set.termΙ = Lean.ParserDescr.node `Set.termΙ 1024 (Lean.ParserDescr.symbol "Ι")