Theorems · Definition · order theory

OrderIso.supIrredLowerSet

{α : Type u_1} → [inst : PartialOrder α] → [Finite α] → α ≃o { s // SupIrred s }

Birkhoff Representation for partial orders. Any partial order is isomorphic to the partial order of sup-irreducible elements in its lattice of lower sets.

Defined in

Mathlib.Order.Birkhoff

Cited by

3 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderFinite