Linear extensions of a finite poset

Let $(P,⪯)$ be a finite poset and write $x\prec y$ for $x⪯y$ with $x\mathrm{\ne }y$, the strict order of Partial order and partially ordered set. A linear extension of $P$ is a tuple $\pi =(x_1,\dots ,x_n)$ that lists every element of $P$ exactly once and is such that $x\prec y$ implies that $x$ occurs before $y$ in $\pi$: that is, $x=x_i$ and $y=x_j$ with $i<j$.

Equivalently, a linear extension is the strict total order $x_1⊏x_2⊏\cdots ⊏x_n$ on the underlying set of $P$ determined by the listing, which extends $\prec$; with respect to it the whole set $P$ is a chain (Chain in a poset). For $x\in P$ the index $i$ with $x=x_i$ is the position of $x$ in $\pi$. Since a linear extension is a listing without repetitions, it has exactly $n$ entries and every element of $P$ occurs exactly once; the empty poset has the empty linear extension $()$.

Nothing else is asserted here: in particular it is not part of the definition that a linear extension exists. For every finite poset existence is proved in Linear extensions of a finite poset: existence, prescribed initial ideals, and adjacent-swap connectivity ↗, which also shows that a prescribed order ideal can be made the initial segment of a linear extension and that any two linear extensions are connected by adjacent interchanges of incomparable elements.