Recursively repetition-free labelled trees preserve Dedekind-finiteness

ID: recursively-repetition-free-labelled-trees-preserve-dedekind-finiteness

If is an infinite Dedekind-finite set, then is another such set. Single-vertex rooted trees inject into it. A countable sequence of distinct rooted trees gives finite lists of labels by the depth-first traversal of a tree in the prescribed child order. By countable union of explicitly ordered finite lists without choice, an infinite union of labels contradicts Dedekind-finiteness. A finite union is equally impossible, since every rooted tree then lies in the finite set , by mathematical induction on using the recursive child rule. Thus no countably infinite subset of rooted trees exists.

New to topics? Read the docs here!