# 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

noncomputable def WellFounded.wellOrderExtension {α : Type u} {r : ααProp} (hwf : ) :

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
instance WellFounded.wellOrderExtension.isWellFounded_lt {α : Type u} {r : ααProp} (hwf : ) :
IsWellFounded α LT.lt
Equations
• =
theorem WellFounded.exists_well_order_ge {α : Type u} {r : ααProp} (hwf : ) :
∃ (s : ααProp), r s

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

def WellOrderExtension (α : Type u_1) :
Type u_1

A type alias for α, intended to extend a well-founded order on α to a well-order.

Equations
Instances For
instance instInhabitedWellOrderExtension {α : Type u} [] :
Equations
• instInhabitedWellOrderExtension = inst
def toWellOrderExtension {α : Type u} :

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

Equations
• toWellOrderExtension =
Instances For
noncomputable instance instLinearOrderWellOrderExtensionOfWellFoundedLT {α : Type u} [LT α] [] :
Equations
• instLinearOrderWellOrderExtensionOfWellFoundedLT = .wellOrderExtension
instance WellOrderExtension.wellFoundedLT {α : Type u} [LT α] [] :
Equations
• =
theorem toWellOrderExtension_strictMono {α : Type u} [] [] :
StrictMono toWellOrderExtension