$
\def\N{\mathbb{N}}
\def\R{\mathbb{R}}
\def\pow{\mathcal{P}}
\def\pown{\pow(\N)}
$
Definitions:
$|A| \le |B|$ if there is an injection from $A$ into $B$;
$|A| = |B|$ if there is a bijection from $A$ onto $B$;
Proposition 0.12 in Real Analysis by Folland (1999), he showed the existence of an injection from $\pown$ to $\R$ by constructing a function $f: \pown \to \R $ such that $$ \forall A \subseteq \N: f(A) = \begin{cases} S(A), & |\N \setminus A| = |\N|\\ 1 + S(A), & |\N \setminus A| < |\N| \end{cases} $$ where $S(A) = \sum_{n \in A} 2^{-n}$. But he did not demonstrate that it is injective. Here is my attempt at a formal proof of it:
Attempt: Let $$ X = \{ A \subseteq \N ~|~ |\N\setminus A| = |\N|\}\\ Y = \{ A \subseteq \N ~|~ |\N\setminus A| < |\N|\} $$ Since $|\N\setminus A| \le |\N|$, $X$ and $Y$ partition $\N$. Moreover, $$ f[X] \subseteq [0, 1)\\ f[Y] \subseteq (1, 2] $$ Hence, it suffices to show that the two restrictions $ f \restriction_X $ and $ f \restriction_Y $ are both injective.
Lemma 1: For any $A \subseteq \N$, $$ |\N\setminus A| = |\N| \leftrightarrow \forall n \in \N: \exists m \in \N: (m > n \land m \notin A) $$ That is, $A$ has infinite holes in $\N$ exactly when $|\N\setminus A| = |\N|$.
Proof: ($\to$) Suppose $\exists n \in \N: \forall m \in \N: [m > n \to m \in A]$. The contrapositive is $m \notin A \to m \le n$, i.e.,
$$
\exists n \in \N: \forall m \in \N \setminus A: m \le n
$$
meaning $\N \setminus A$ is bounded, by which there cannot be a bijection between $\N \setminus A$ and $\N$.
($\leftarrow$) Let $B = \N\setminus A$ for brevity. Let $(C_n)_{n \in \N}$ be defined by $C_n = \{m \in B ~|~ m > n\} \subseteq \N$. By the condition, $C_n$ is nonempty for all $n \in \N$. So we can define a function $g: \N \to B$ such that
$$
\forall n \in \N: g(n) = \min C_n
$$
Since $g(n) > n$, $g$ is injective. Furthurmore, $B \subseteq \N$ implies $|B| \le |\N|$. By the Schroeder-Bernstein theorem, $|B| = |\N|$.
By Lemma 1, we also have
Corollary 1: $ |\N\setminus A| < |\N| \leftrightarrow \exists n \in \N: \forall m > n: m \in A $
Lemma 2: For all $A, B \subseteq \N$, If $A \neq B$ and $S(A) = S(B)$, then, there is $n \in \N$ such that
- $\forall i < n: (i \in A \leftrightarrow i \in B)$
- $n \notin A \land \forall i > n: i \in A \land n \in B \land \forall i > n: i \notin B $ WLOG
I failed to show Lemma 2, but assume for now it holds.
For all $A, B \in X$, aiming for a contradiction, suppose that $A \neq B$ and $S(A) = S(B)$. Then, Lemma 1 and 2 yield a contradiction.
For all $A, B \in Y$, suppose that $A \neq B$ and $S(A) = S(B)$. Then, Corollary 1 and Lemma 2 yield a contradiction.
Therefore, $f$ is injective.
Questions:
We know that two numbers $0.1_2$ and $0.0\bar{1}_2$ have different expansions but the values are identical. I designed Lemma 2 to say that it is the only way that any numbers with distinct binary expansions have the same value. Is Lemma 2 true and how to show it?
Given that Lemma 2 is true, is the proof valid?