Extend a partial order to a linear order #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file constructs a linear order which is an extension of the given partial order, using Zorn's lemma.
Any partial order can be extended to a linear order.
A type alias for α, intended to extend a partial order on α to a linear order.
Equations
- linear_extension α = α
Instances for linear_extension
@[protected, instance]
Equations
- linear_extension.linear_order = {le := linear_extension.linear_order._proof_1.some, lt := partial_order.lt._default linear_extension.linear_order._proof_1.some, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le), max := max_default (λ (a b : linear_extension α), classical.dec_rel has_le.le a b), max_def := _, min := min_default (λ (a b : linear_extension α), classical.dec_rel has_le.le a b), min_def := _}
The embedding of α into linear_extension α as a relation homomorphism.
Equations
- to_linear_extension = {to_fun := λ (x : α), x, map_rel' := _}
@[protected, instance]
Equations
- linear_extension.inhabited = {default := inhabited.default _inst_1}