# 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*function`WellFounded.rank : α → Ordinal`

. - the second map is injective but doesn't necessarily respect the order. This is an arbitrary
embedding into
`Cardinal`

given by`embeddingToCardinal`

.

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`

instead of `Cardinal`

. The new definition is definitionally equal to the `mathlib`

3 version but
avoids non-standard instances.

## Tags #

well founded relation, well order, extension

An arbitrary well order on `α`

that extends `r`

.

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 `r`

.

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.

## Equations

- hwf.wellOrderExtension = LinearOrder.lift' (fun (a : α) => (hwf.rank a, embeddingToCardinal a)) ⋯

## Instances For

## Equations

- ⋯ = ⋯

Any well-founded relation can be extended to a well-ordering on that type.

A type alias for `α`

, intended to extend a well-founded order on `α`

to a well-order.

## Equations

- WellOrderExtension α = α

## Instances For

## Equations

- instInhabitedWellOrderExtension = inst

"Identity" equivalence between a well-founded order and its well-order extension.

## Equations

- toWellOrderExtension = Equiv.refl α

## Instances For

## Equations

- instLinearOrderWellOrderExtensionOfWellFoundedLT = ⋯.wellOrderExtension

## Equations

- ⋯ = ⋯