Extend a well-founded order to a well-order #
This file constructs a well-order (linear well-founded order) which is an extension of a given well-founded order.
Proof idea #
We can map our order into two well-orders:
- the first map respects the order but isn't necessarily injective. Namely, this is the rank
WellFounded.rank : α → Ordinal.
- the second map is injective but doesn't necessarily respect the order. This is an arbitrary
Then their lexicographic product is a well-founded linear order which our original order injects in.
Porting notes #
The definition in
mathlib 3 used an auxiliary well-founded order on
α lifted from
Cardinal. The new definition is definitionally equal to the
mathlib 3 version but
avoids non-standard instances.
well founded relation, well order, extension
An arbitrary well order on
α that extends
The construction maps
r into two well-orders: the first map is
WellFounded.rank, which is not
necessarily injective but respects the order
r; the other map is the identity (with an arbitrarily
chosen well-order on
α), which is injective but doesn't respect
By taking the lexicographic product of the two, we get both properties, so we can pull it back and
get a well-order that extend our original order
r. Another way to view this is that we choose an
arbitrary well-order to serve as a tiebreak between two elements of same rank.