Lexicographic order on finitely supported dependent functions #
This file defines the lexicographic order on DFinsupp
.
DFinsupp.Lex r s
is the lexicographic relation on Π₀ i, α i
, where ι
is ordered by r
,
and α i
is ordered by s i
.
The type synonym Lex (Π₀ i, α i)
has an order given by DFinsupp.Lex (· < ·) (· < ·)
.
Instances For
The partial order on DFinsupp
s obtained by the lexicographic ordering.
See DFinsupp.Lex.linearOrder
for a proof that this partial order is in fact linear.
The less-or-equal relation for the lexicographic ordering is decidable.
Instances For
The less-than relation for the lexicographic ordering is decidable.
Instances For
The linear order on DFinsupp
s obtained by the lexicographic ordering.
We are about to sneak in a hypothesis that might appear to be too strong.
We assume CovariantClass
with strict inequality <
also when proving the one with the
weak inequality ≤
. This is actually necessary: addition on Lex (Π₀ i, α i)
may fail to be
monotone, when it is "just" monotone on α i
.