English
Let α be a finite poset. Then every inf-irreducible upper set in the lattice of upper sets is of the form Ici(a) for some a ∈ α. Equivalently, the map infIrredUpperSet : α → { s : UpperSet α // InfIrred s } is surjective.
Русский
Пусть α — конечная частично упорядоченная функция. Тогда любая инф-нередуцируемая верхняя часть в решётке верхних множеств имеет вид Ici(a) для некоторого a ∈ α.
LaTeX
$$$\\operatorname{Surjective}(\\operatorname{infIrredUpperSet}_{\\alpha})$$$
Lean4
/-- **Birkhoff Representation for partial orders.** Any partial order is isomorphic
to the partial order of inf-irreducible elements in its lattice of upper sets. -/
noncomputable def infIrredUpperSet : α ≃o { s : UpperSet α // InfIrred s } :=
RelIso.ofSurjective _ OrderEmbedding.infIrredUpperSet_surjective
