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.

ink

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

Any partial order can be extended to a linear order.

ink

def LinearExtension (α : Type u) : Type u

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

Equations

• LinearExtension α = α

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

def toLinearExtension {α : Type u} [inst : PartialOrder α] : (fun x x_1 => x ≤ x_1) →r fun x x_1 => x ≤ x_1

The embedding of α into LinearExtension α as a relation homomorphism.

Equations

• toLinearExtension = { toFun := fun x => x, map_rel' := (_ : ∀ {a b : α}, (fun x x_1 => x ≤ x_1) a b ≤ Exists.choose (_ : ∃ s x, (fun x x_1 => x ≤ x_1) ≤ s) a b) }

ink

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

Equations

• instInhabitedLinearExtension = { default := default }