Is there a name for this type of poset? In two unrelated papers that I am writing, I have come across the following type of poset:
Assumption. Let $(I,\leq)$ be a poset. Assume that for every $i \in I$ the set $I_{\leq i} = \{j \in I\ |\ j \leq i\}$ is finite.
This type of poset is useful for induction arguments: you can carry out constructions by induction on the size of $I_{\leq i}$. The type of application I have in mind is the following:
Application. Given a functor $F \colon I^{\operatorname{op}} \to \mathscr C$ to some category $\mathscr C$ with fibre products, and given a subcategory $\mathscr C' \subseteq \mathscr C$ of 'nice' objects such that every object of $\mathscr C$ is 'covered' (noncanonically) by an object of $\mathscr C'$, one can construct a covering $G \colon I^{\operatorname{op}} \to \mathscr C'$ of $F$ by induction as follows: for $i$ minimal choose any cover $G(i) \to F(i)$ with $G(i) \in \mathscr C'$. In general, if $I_{\leq i} = \{j_1,\ldots,j_r\}$, choose $G(i) \in \mathscr C'$ as a cover of
$$F(i) \underset{F(j_1)}\times G(j_1) \underset{F(j_2)}\times \cdots \underset{F(j_r)}\times G(j_r),$$
which by construction admits maps to each $G(j_k)$ for $k \in \{1,\ldots,r\}$ making all the necessary diagrams commute.
Question. Do these posets have a standard (or non-standard!) name in the literature?
I would also be interested in a systematic study of directed posets with this property. The standard example is the poset of finite subsets of a given set. Is there a sense in which every example comes from one of these?
 A: I feel like a standard name for such posets ought to exist, but I have never heard of one and haven't been able to find one with a bit of searching.  Here are some things I can say though.
Such a partial on a set $I$ is equivalent to a $T_0$ topology which is locally finite (i.e., in which every point has a finite neighborhood).  If you replace "partial order" with "preorder" then that is equivalent to dropping the $T_0$ assumption.  Explicitly, given such a poset $(I,\leq)$, define a topology by saying $U\subseteq I$ is open iff for all $i\in U$, $j\leq i$ implies $i\in U$.  Conversely, the ordering $\leq$ can be recovered as the specialization order of the topology (or its opposite, depending on your conventions).
Unfortunately, the term "locally finite poset" has a different standard meaning (it means that the interval between any two elements is finite), so you can't borrow that name from topology.  This definition is closely related to yours, though: a poset has your property iff the poset obtained by adjoining a least element is locally finite.
In the directed case, there is indeed a close connection with the poset of finite subsets of a set: any such directed partial poset $I$ embeds cofinally in the poset of finite subsets of a set.  Namely, it embeds in the finite subsets of $I$ itself, by sending $i\in I$ to the set $I_{\leq i}$.  This embedding is cofinal precisely because $I$ is directed.  Conversely, any cofinal subset of the poset of finite subsets of a set is a directed poset of this type, so this is a complete characterization of such posets.
If you drop the directed assumption, then your posets can similarly be characterized as the posets that embed in the poset of finite subsets of some set.
