English
Any finite poset α is order-isomorphic to the lattice of sup-irreducible lower sets in its lattice of lower sets. More precisely, there exists an order isomorphism supIrredLowerSet : α ≃o { s : LowerSet α // SupIrred s }.
Русский
Любое конечное частично упорядоченное множество α изоморфно решётке суп-нередуцируемых нижних множеств в её решётке нижних множеств. Точнее, существует изоморфизм порядка supIrredLowerSet : α ≃o { s : LowerSet α // SupIrred s }.
LaTeX
$$$\\alpha \\cong_o \\{ s : \\mathrm{LowerSet}(\\alpha) \\mid \\mathrm{SupIrred}(s) \\}$$$
Lean4
/-- **Birkhoff Representation for partial orders.** Any partial order is isomorphic
to the partial order of sup-irreducible elements in its lattice of lower sets. -/
noncomputable def supIrredLowerSet : α ≃o { s : LowerSet α // SupIrred s } :=
RelIso.ofSurjective _ OrderEmbedding.supIrredLowerSet_surjective
