Extend a partial order to a linear order

This file constructs a linear order which is an extension of the given partial order, using Zorn's lemma.

theorem extend_partialOrder {α : Type u} (r : α → α → Prop) [IsPartialOrder α r] : ∃ (s : α → α → Prop), IsLinearOrder α s ∧ r ≤ s

Any partial order can be extended to a linear order.

def LinearExtension (α : Type u) : Type u

A type alias for α, intended to extend a partial order on α to a linear order.

Equations

• LinearExtension α = α

noncomputable instance instLinearOrderLinearExtensionOfPartialOrder {α : Type u} [PartialOrder α] : LinearOrder (LinearExtension α)

Equations

• instLinearOrderLinearExtensionOfPartialOrder = LinearOrder.mk ⋯ (Classical.decRel fun (x1 x2 : LinearExtension α) => x1 ≤ x2) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

def toLinearExtension {α : Type u} [PartialOrder α] : α →o LinearExtension α

The embedding of α into LinearExtension α as an order homomorphism.

Equations

• toLinearExtension = { toFun := fun (x : α) => x, monotone' := ⋯ }

instance instInhabitedLinearExtension {α : Type u} [Inhabited α] : Inhabited (LinearExtension α)

Equations

• instInhabitedLinearExtension = { default := default }