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 IsWellFounded.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 IsWellFounded.wellOrderExtension {α : Type u} (r : α → α → Prop) [IsWellFounded α r] : LinearOrder α

An arbitrary well order on α that extends r.

The construction maps r into two well-orders: the first map is IsWellFounded.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

• IsWellFounded.wellOrderExtension r = LinearOrder.lift' (fun (a : α) => (IsWellFounded.rank r a, embeddingToCardinal a)) ⋯

instance IsWellFounded.wellOrderExtension.isWellFounded_lt {α : Type u} (r : α → α → Prop) [IsWellFounded α r] : IsWellFounded α LT.lt

Equations

• ⋯ = ⋯

instance IsWellFounded.wellOrderExtension.isWellOrder_lt {α : Type u} (r : α → α → Prop) [IsWellFounded α r] : IsWellOrder α LT.lt

Equations

• ⋯ = ⋯

theorem IsWellFounded.exists_well_order_ge {α : Type u} (r : α → α → Prop) [IsWellFounded α r] : ∃ (s : α → α → Prop), r ≤ s ∧ IsWellOrder α s

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

@[deprecated IsWellFounded.wellOrderExtension]

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

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)) ⋯

@[deprecated IsWellFounded.wellOrderExtension.isWellFounded_lt]

instance WellFounded.wellOrderExtension.isWellFounded_lt {α : Type u} {r : α → α → Prop} (hwf : WellFounded r) : IsWellFounded α LT.lt

Equations

• ⋯ = ⋯

@[deprecated IsWellFounded.exists_well_order_ge]

theorem WellFounded.exists_well_order_ge {α : Type u} {r : α → α → Prop} (hwf : WellFounded r) : ∃ (s : α → α → Prop), r ≤ s ∧ IsWellOrder α 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

• WellOrderExtension α = α

instance instInhabitedWellOrderExtension {α : Type u} [Inhabited α] : Inhabited (WellOrderExtension α)

Equations

• instInhabitedWellOrderExtension = inst

def toWellOrderExtension {α : Type u} : α ≃ WellOrderExtension α

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

Equations

• toWellOrderExtension = Equiv.refl α

noncomputable instance instLinearOrderWellOrderExtensionOfWellFoundedLT {α : Type u} [LT α] [h : WellFoundedLT α] : LinearOrder (WellOrderExtension α)

Equations

• instLinearOrderWellOrderExtensionOfWellFoundedLT = IsWellFounded.wellOrderExtension fun (x1 x2 : α) => x1 < x2

instance WellOrderExtension.wellFoundedLT {α : Type u} [LT α] [WellFoundedLT α] : WellFoundedLT (WellOrderExtension α)

Equations

• ⋯ = ⋯

theorem toWellOrderExtension_strictMono {α : Type u} [Preorder α] [WellFoundedLT α] : StrictMono ⇑toWellOrderExtension