mathlib documentation

order.extension

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_partial_order {α : Type u} (r : α → α → Prop) [is_partial_order α r] :
∃ (s : α → α → Prop) (_x : is_linear_order α s), r s

Any partial order can be extended to a linear order.

def linear_extension (α : Type u) :
Type u

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

Equations
Instances for linear_extension
@[protected, instance]
noncomputable def linear_extension.linear_order {α : Type u} [partial_order α] :
Equations

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

Equations
@[protected, instance]
Equations