The Polish space of trees and its well-founded rank

Assume ZFC, with The Axiom of Choice supplying the hypothesis of the closed-subspace Polishness result below. Enumerate ${\mathbb{N}}^{<\omega }$ by increasing length plus sum of entries, then by length and lexicographically within each finite stratum. This is a bijection with $\mathbb{N}$. Identify subsets of finite words with their characteristic binary sequences, and let $\mathrm{T}\mathrm{r}$ consist of the prefix-closed subsets, including the empty tree, as in Trees and their bodies. Give it the inherited Cantor topology from Cantor and Baire sequence spaces and coordinate codings.

The space $\mathrm{T}\mathrm{r}$ is closed: failure of prefix closure is witnessed by two words $t\in T$, $s\subseteq t$ with $s\mathrm{\notin }T$, and fixing these two characteristic coordinates gives an open neighbourhood of non-trees. It is therefore Polish by Closed subspaces, products, and Baire parametrization.

Let $\mathrm{W}\mathrm{F}\subseteq \mathrm{T}\mathrm{r}$ consist of trees whose immediate-child relation, with a child related to its parent, is well-founded. This relation is setlike. For $T\in \mathrm{W}\mathrm{F}$, Ordinal rank of a well-founded relation defines

$r_T(s)=\sup \{r_T(s^{⌢}n)+1:s^{⌢}n\in T\}\mathrm{.}$

Its supplier proves existence and ordinal-valuedness with a total recursion rule; the empty supremum is zero. Put $r(T)=r_T(\mathrm{\varnothing })$ for nonempty T and $r(\mathrm{\varnothing })=0$ for the empty tree. Thus both an empty tree and a root-only tree have rank zero. The rank does not distinguish those trees. We do not assign a negative ordinal rank to the empty tree. Write $\mathrm{I}\mathrm{F}=\mathrm{T}\mathrm{r}\setminus \mathrm{W}\mathrm{F}$; its identification with trees having infinite branches is proved separately.