Lexicographic order on Pi types #
This file defines the lexicographic order for Pi types.
a is less than
a i = b i for all
i up to some point
a k < b k.
Πₗ i, α i: Pi type equipped with the lexicographic order. Type synonym of
Π i, α i.
See also #
Related files are:
If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.