User:Hakerh400/Schröder–Bernstein theorem

Schröder–Bernstein theorem states that for any two sets $A$ and $B$, if there exists an injective function from $A$ to $B$ and an injective function from $B$ to $A$, then there exists a bijective function between $A$ and $B$. There are many proofs of this theorem. In this article we present one of the simplest and most natural proofs. We hope this proof is easier to follow and understand than most of the other proofs. This proof has been formally verified using an interactive theorem prover.

Definitions

Given two sets $A$ and $B$. Given injective functions $f:A\mapsto B$ and $g:B\mapsto A$. We want to construct a bijective function $R:A\mapsto B$.

Let $F$ and $G$ be two infinite sequences such that $F_{0}=G_{0}=\emptyset$, and for any $n\in \mathbb {N}$, $G_{n+1}$ is defined as

$G_{n+1}=B\setminus \left(\bigcup _{i=0}^{n}G_{i}\right)\setminus f\left[A\setminus \bigcup _{i=0}^{n}F_{i}\right]$

and $F_{n+1}=g\left[G_{n+1}\right]$. Notation $h[X]$ represents the image of set $X$ under function $h$.
Let $A'=A\setminus \bigcup _{i\in \mathbb {N} }F_{i}$ and $B'=B\setminus \bigcup _{i\in \mathbb {N} }G_{i}$. We define function $R$ such that for all $x\in A$:

$R(x)={\begin{cases}f(x),&x\in A'\\g^{-1}(x),&{\text{otherwise}}\end{cases}}$

The goal is to prove that $R$ is a bijection between $A$ and $B$.

Proof sketch

The proof consists of several steps:

1. Prove that for all $m,n\in \mathbb {N}$, if $m\neq n$ then $F_{m}$ and $F_{n}$ are disjoint (also applies to $G_{m}$ and $G_{n}$)
2. Prove that $g$ is a bijection between $G_{n}$ and $F_{n}$ for all $n\in \mathbb {N}$ (this holds because $F_{n}$ is an image of $G_{n}$ under $g$, and $g$ is injective)
3. From 2. it follows that $g^{-1}$ is well-defined and also a bijection between $F_{n}$ and $G_{n}$ for all $n\in \mathbb {N}$
4. Prove that $f$ is a bijection between $A'$ and $B'$ (this is the hardest step)
5. Since $A'$ is disjoint from $F_{n}$ for all $n\in \mathbb {N}$ (also applies to $B'$ and $G_{n}$), then $R$ is a bijection between $A$ and $B$