= Finite repetition-free sequences preserve Dedekind-finiteness
If $X$ is a <Dedekind-finite set>, its <set> of <finite repetition-free sequences> is also Dedekind-finite. An injective <sequence> of distinct finite lists would, by <countable union of explicitly ordered finite lists without choice>, either produce an injection $\mathbb N\to X$ or use only finitely many entries. The latter possibility is impossible because a fixed finite pool supports only finitely many repetition-free lists. If $X$ is infinite, the one-entry lists also show that the resulting <set> is infinite.
Back to article page
