Theorems · Definition · order theory

OrderIso.infIrredUpperSet

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

Birkhoff Representation for partial orders. Any partial order is isomorphic to the partial order of inf-irreducible elements in its lattice of upper 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