mathlib3 documentation


Extend a well-founded order to a well-order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

noncomputable def well_founded.well_order_extension {α : Type u} {r : α α Prop} (hwf : well_founded r) :

An arbitrary well order on α that extends r.

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

@[protected, instance]
theorem well_founded.exists_well_order_ge {α : Type u} {r : α α Prop} (hwf : well_founded r) :
(s : α α Prop), r s is_well_order α s

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

def well_order_extension (α : Type u_1) :
Type u_1

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

Instances for well_order_extension
@[protected, instance]

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

@[protected, instance]