mathlib3documentation

order.extension.well

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:

• the first map respects the order but isn't necessarily injective. Namely, this is the rank function rank : α → ordinal.
• the second map is injective but doesn't necessarily respect the order. This is an arbitrary well-order on α.

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.

Equations
@[protected, instance]
theorem well_founded.exists_well_order_ge {α : Type u} {r : α α Prop} (hwf : well_founded r) :
(s : α α Prop), r 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.

Equations
Instances for well_order_extension
@[protected, instance]
Equations
def to_well_order_extension {α : Type u} :

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

Equations
@[protected, instance]
noncomputable def well_order_extension.linear_order {α : Type u} [has_lt α]  :
Equations
@[protected, instance]