Documentation

Mathlib.Order.Extension.Linear

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

Szpilrajn extension theorem: any partial order can be extended to a linear order.

def LinearExtension (α : Type u) :

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

Equations
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def toLinearExtension {α : Type u} [PartialOrder α] :

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

Equations