Intervals in pi-space #
In this we prove various simple lemmas about intervals in Π i, α i. Closed intervals (Ici x,
Iic x, Icc x y) are equal to products of their projections to α i, while (semi-)open intervals
usually include the corresponding products as proper subsets.
If x, y, x', and y' are functions Π i : ι, α i, then
the set difference between the box [x, y] and the product of the open intervals (x' i, y' i)
is covered by the union of the following boxes: for each i : ι, we take
[x, update y i (x' i)] and [update x i (y' i), y].
E.g., if x' = x and y' = y, then this lemma states that the difference between a closed box
[x, y] and the corresponding open box {z | ∀ i, x i < z i < y i} is covered by the union
of the faces of [x, y].
If x, y, z are functions Π i : ι, α i, then
the set difference between the box [x, z] and the product of the intervals (y i, z i]
is covered by the union of the boxes [x, update z i (y i)].
E.g., if x = y, then this lemma states that the difference between a closed box
[x, y] and the product of half-open intervals {z | ∀ i, x i < z i ≤ y i} is covered by the union
of the faces of [x, y] adjacent to x.