As part of a proof that the long line is locally Euclidean, I'd like to prove the following:
Proposition. If $A$ is a countable well-ordered set, then $A \times [0,1)$ with the dictionary order is homeomorphic to $[0,1)$.
My proof is below. I'd like to know if this proof is correct and if there's a prettier proof out there.
Proof. For each $\alpha \in A$, pick $\epsilon_\alpha > 0$ so that $\sum_{\alpha \in A} \epsilon_\alpha = 1$. Define $f: A \times [0,1) \to [0,1)$ by $$ f(\alpha, t) = t\epsilon_\alpha + \sum_{\beta < \alpha}\epsilon_\beta. $$ It's not hard to see that if $(\alpha_1,t_1) < (\alpha_2,t_2)$, then $f(\alpha_1,t_1) < f(\alpha_2,t_2)$. Thus $f$ is injective and if we can show it's surjective, it will automatically be a homeomorphism.
$X := f(A \times [0,1))$ is a disjoint union of intervals with lengths $\epsilon_\alpha$, so $X$ has Lebesgue measure $1$ and is therefore dense in $[0,1)$. Let $x \in [0,1)$ be arbitrary; we'll show that $x \in X$. If $x=0$ then we're done, since then $x = f(\alpha_0, 0)$ where $\alpha_0$ is the smallest element of $A$. So assume $x \in (0,1)$. For all $\alpha \in A$, let $$ x_\alpha := \sum_{\beta < \alpha} \epsilon_\beta = f(\alpha, 0). $$ Since $X$ is dense, for all $n \in \mathbb{N}$ we can find some $f(\alpha_n', t) \in (x-1/n,x]$. Let $\alpha_n$ be the successor of $\alpha_n'$. If $x \leq x_{\alpha_n'}$, then clearly $x \in [x_{\alpha_n'}, x_{\alpha_n}] \subseteq X$. Otherwise, $x_{\alpha_n} \in (x-1/n,x)$. We thus get a sequence $(x_{\alpha_n})$ which converges to $x$. Pick an increasing subsequence and rename it $(x_{\alpha_n})$; we still have $x_{\alpha_n} \to x$.
We'll show that $x_{\alpha_n} \to x_\alpha$, where $\alpha$ is the smallest element of $A$ greater than all the $\alpha_n$. Since $[0,1)$ is Hausdorff, it will follow that $x = x_\alpha$, and we'll be done. Clearly $x \leq x_\alpha$ since all $x_{\alpha_n} < x_\alpha$. For the reverse direction, let $y < x_\alpha$ be arbitrary. Then by the definition of $x_\alpha$, there exists a finite collection $\{\beta_1,\ldots,\beta_k\} \subseteq A$ with all $\beta_i < \alpha$ such that $\sum_{i=1}^k \epsilon_{\beta_i} > y$. By the definition of $\alpha$ and the fact that $(\alpha_n)$ is increasing, there exists some $\alpha_n$ greater than all the $\beta_i$. It then follows that $$ y < \sum_i \epsilon_{\beta_i} \leq x_{\alpha_n} \leq x. $$ Since $y$ was arbitrary, we have $x \geq x_\alpha$, and we conclude that $x = x_\alpha$.
Proof: without loss of generality, take $A$ to be an ordinal. We proceed by transfinite induction. Note we need to add the hypothesis that $A$ is nonempty.
When we have a totally ordered set $I$ and, for each $i \in I$, a totally ordered set $S_i$, we can form the “sum order” $\sum\limits_{i \in I} S_i$, whose underlying set is $\coprod\limits_{i \in I} S_i$ and which is ordered first by $i$, then by the order of $S_i$. In the case where $I$ is well-ordered and each $S_i$ is well-ordered, this gives a well-ordered set, which is identified with its order type. As a special case, $S_1 + S_2 := \sum\limits_{i \in \{1, 2\}} S_i$. Note that sums left-distribute over products.
Base case: $A = 1$. Trivial.
Inductive step 1: $A = B + 1$. In this case, we see that $(B + 1) \times [0, 1) \cong B \times [0, 1) + 1 \times [0, 1) \cong [0, 1) + [0, 1) \cong [0, 1) + [1, 2) \cong [0, 2) \cong [0, 1).$
Inductive step 2: $A$ is a limit ordinal. Then $A$ has cofinality $\omega$, which means we can write $A = \sum\limits_{i = 0}^\infty B_i$ where $B_i < A$ for all $i$. Then we have $A \times [0, 1) = (\sum\limits_{n \in \mathbb{N}} B_i) \times [0, 1) \cong \sum\limits_{i \in \mathbb{N}} (B_i \times [0, 1)) \cong \sum\limits_{i \in \mathbb{N}} [0, 1) \cong \sum\limits_{i \in \mathbb{N}} [i, i + 1) \cong [0, \infty) \cong [0, 1).$