Lexicographic order on Pi types #
This file defines the lexicographic and colexicographic orders for Pi types.
- In the lexicographic order,
a
is less thanb
ifa i = b i
for alli
up to some pointk
, anda k < b k
. - In the colexicographic order,
a
is less thanb
ifa i = b i
for alli
above some pointk
, anda k < b k
.
Notation #
Πₗ i, α i
: Pi type equipped with the lexicographic order. Type synonym ofΠ i, α i
.
See also #
Related files are:
The lexicographic relation on Π i : ι, β i
, where ι
is ordered by r
,
and each β i
is ordered by s
.
The <
relation on Lex (∀ i, β i)
is Pi.Lex (· < ·) (· < ·)
, while the <
relation on
Colex (∀ i, β i)
is Pi.Lex (· > ·) (· < ·)
.
Instances For
The notation Πₗ i, α i
refers to a pi type equipped with the lexicographic order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Pi.instPartialOrderLexForallOfLinearOrder = partialOrderOfSO fun (x1 x2 : Lex ((i : ι) → β i)) => x1 < x2
Equations
- Pi.instPartialOrderColexForallOfLinearOrder = partialOrderOfSO fun (x1 x2 : Colex ((i : ι) → β i)) => x1 < x2
Lex (∀ i, α i)
is a linear order if the original order has well-founded <
.
Equations
- Pi.Lex.linearOrder = linearOrderOfSTO fun (x1 x2 : Lex ((i : ι) → (fun (i : ι) => β i) i)) => x1 < x2
Colex (∀ i, α i)
is a linear order if the original order has well-founded >
.
Equations
Equations
- Pi.instBoundedOrderLexForallOfWellFoundedLT = { toOrderTop := Pi.instOrderTopLexForallOfWellFoundedLT, toOrderBot := Pi.instOrderBotLexForallOfWellFoundedLT }
Equations
- Pi.instBoundedOrderColexForallOfWellFoundedGT = { toOrderTop := Pi.instOrderTopColexForallOfWellFoundedGT, toOrderBot := Pi.instOrderBotColexForallOfWellFoundedGT }
If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.
If we swap two strictly increasing values in a function, then the result is colexicographically smaller than the original function.