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.

source

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

linear_order α

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

hwf.well_order_extension = let l : linear_order α := is_well_order.linear_order well_ordering_rel in linear_order.lift' (λ (a : α), (hwf.rank a, a)) _

source

@[protected, instance]

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

is_well_founded α linear_order.lt

source

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.

source

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

well_order_extension α = α

Instances for well_order_extension

source

@[protected, instance]

def well_order_extension.inhabited {α : Type u} [inhabited α] :

inhabited (well_order_extension α)

Equations

well_order_extension.inhabited = _inst_1

source

def to_well_order_extension {α : Type u} :

α ≃ well_order_extension α

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

Equations

to_well_order_extension = equiv.refl α

source

@[protected, instance]

noncomputable def well_order_extension.linear_order {α : Type u} [has_lt α] [well_founded_lt α] :

linear_order (well_order_extension α)

Equations

well_order_extension.linear_order = well_order_extension.linear_order._proof_1.well_order_extension

source

@[protected, instance]

def well_order_extension.well_founded_lt {α : Type u} [has_lt α] [well_founded_lt α] :

well_founded_lt (well_order_extension α)

source

theorem to_well_order_extension_strict_mono {α : Type u} [preorder α] [well_founded_lt α] :

strict_mono ⇑to_well_order_extension