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:

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 : WellFounded r) :

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.

  • hwf.wellOrderExtension = LinearOrder.lift' (fun (a : α) => (hwf.rank a, embeddingToCardinal a))
Instances For
    instance WellFounded.wellOrderExtension.isWellFounded_lt {α : Type u} {r : ααProp} (hwf : WellFounded r) :
    IsWellFounded α
    • =
    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.

    Instances For
      • instInhabitedWellOrderExtension = inst

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

      Instances For
        • instLinearOrderWellOrderExtensionOfWellFoundedLT = .wellOrderExtension
        theorem toWellOrderExtension_strictMono {α : Type u} [Preorder α] [WellFoundedLT α] :
        StrictMono toWellOrderExtension