English
Let α be a finite partially ordered set. Then every sup-irreducible lower set in the lattice of lower sets of α is principal, i.e., there exists a ∈ α with s = Iic(a). Equivalently, the map supIrredLowerSet : α → { s : LowerSet α // SupIrred s } is surjective.
Русский
Пусть α — конечная частично упорядоченная множество. Тогда любая суп-нередуцируемая нижняя часть в решётке нижних множеств α является порожденной элементом: существует a ∈ α такое, что s = Iic(a). Эквивалентно, отображение supIrredLowerSet : α → { s : LowerSet α // SupIrred s } сюръективно.
LaTeX
$$$\\operatorname{Surjective}(\\operatorname{supIrredLowerSet}_{\\alpha})$$$
Lean4
theorem supIrredLowerSet_surjective : Surjective (supIrredLowerSet (α := α)) := by aesop (add simp Surjective)
