This seems to me to be equivalent to Koenig's lemma: every infinite, finitely branching tree has an infinite branch. The set of vertices is the disjoint union of all the S_n, and there is an edge from (a,i) to (b,i+1) if f_i(b)=a. Conversely, let S_n be the set of vertices at depth n. -- Peter Tom Leinster wrote:
I've recently come across the following curious little result. I know how to prove it and have a use for it, but my question is: can anyone supply a wider context or explanation?
The result is that the limit in Set of any diagram
... ---> S_3 ---> S_2 ---> S_1
of finite nonempty sets is nonempty. Note that finiteness cannot be dropped: for instance, take each S_n to be the natural numbers and each map to be addition of 1.
Thanks, Tom