The SchrÃ¶der-Bernstein theorem is one of most fundamental facts in set theory. Here we give an easy-to-follow proof of it.

Let \(f: X \rightarrow Y\) and \(g: Y \rightarrow X\) be injective. To find a bijection \(h: X \rightarrow Y\), first we define a couple of sequences of sets, \(\{A_n \subset X \mid n \in \mathbb{N}\}\) and \(\{B_n \subset Y \mid n \in \mathbb{N}\},\) as follows:

\[A_0 := X \setminus g[Y] = \{x \in X \mid \not \exists y \in Y (x = g(y))\};\]\[B_0 := Y \setminus f[X] = \{y \in Y \mid \not \exists x \in X (f(x) = y)\};\]\[A_{n+1} := g[B_n];\]\[B_{n+1} := f[A_n].\]

Note that \(A_n\) are pairwise disjoint for different \(n\)s and \(B_n\) are too, which are provable by simultaneous induction on \(n\), because \(f\) and \(g\) are injective.

Define \(h: X \rightarrow Y\) by:

\[h(x) := \begin{cases}g^{-1}(x) & \text{if}\ x \in A_{2n+1} \text{for some}\ n\\f(x) & \text{otherwise}\end{cases}\]

which is well-defined since the restriction of \(g\) to \(B_{2n}\) is onto \(A_{2n+1}\).

The following figure illustrates the above definitions:

Our proof is done by remarking that \(f[X \setminus \bigcup \{A_n \mid n \in \mathbb{N}\}] = Y \setminus \bigcup \{B_n \mid n \in \mathbb{N}\}\) (and, of course symmmetrically \(g[Y \setminus \bigcup \{B_n \mid n \in \mathbb{N}\}] = X \setminus \bigcup \{A_n \mid n \in \mathbb{N}\},\) too).

It is now straightforward to see why the resulting bijection is not computable in general even with the original pair of injections as oracles; given \(x \in X\), you cannot decide whether \(x\) belongs to \(A_{2n+1}\) for some \(n\) or not in finitely many steps. Yet the above proof does not employ the axiom of choice.

One more thing to note is that fixed points of \(g \circ f\) are, if any, always outside of \(A_n\)s. More generally, any periodic point of \(g \circ f\) resides outside of \(A_n\)s.

This site has been mostly static as of today, but these days it seems no longer a durable excuse for not making SSL connection available. So today we have turned fixedpoint.jp's SSL on thanks to Let's Encrypt and EFF's Certbot. HTTP (port 80) access to our site is now deprecated, but still alive for backward compatibility. Come and enjoy HTTPS.

2018: Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2017: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2016: Dec / Nov / Sep / Aug / Jul / Mar / Feb / Jan

2015: Dec / Oct / Sep / Jul / May / Mar / Feb

2014: Dec / Nov / Oct / Aug / Apr / Mar / Feb / Jan

2013: Dec / Nov / Oct / Sep / Aug / Jun / May / Apr / Mar

2012: Nov / Oct / Sep / Jul / Jun / May / Mar / Feb / Jan

2011: Dec / Nov / Oct / Sep / Jul / Jun / Apr / Mar / Feb / Jan

2010: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2009: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2008: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2007: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

© 2006-2018 fixedpoint.jp