Locally finite poset

Remarks

Example: $\N^k$ with the product order is locally finite. Check: if $x \le y$, the interval $[x, y]$ is the box $\prod_{i=1}^k \set{x_i, \ldots, y_i}$, which has $\prod_i (y_i - x_i + 1)$ elements; if $x \not\le y$, it is empty.

Non-example: $\Q$ with the usual order is not locally finite, since $[0, 1]$ is infinite.

Every finite poset is locally finite. The interval $[x, y]$ is empty unless $x \le y$, so only comparable pairs matter. In Mathlib the class LocallyFiniteOrder provides the intervals as finite sets.