#まえがき
これはQiita 数学 Advent Calendar 2015 クリスマスイブの記事です。

数学のアドベントカレンダー眺めてたらなんとなく書きたくなりました、本当は圏論（最近モナドとクライスリ圏に二重の意味ではまっていた）と絵算のことをこっそり書こうかと思いましたが何も準備してなかったので手帳にメモしてた命題をまとめて見ようかなと思い筆をとった次第です。
、、、問題は今年の１月の日付なのでミスが散見されるかもしれません、平にご容赦（あるいは温かい修正コメントを）下さいませ。
オリジナルな議論はこちらです、勉強になりました。

説明に（正しくないかもしれない）Haskell風な書き方も一部使ってみています。
途中で飽きたので少ししかありませんが。

あと、以下の文ではオーバーロードを
wikiの多重定義
の意味で更に素朴に使っています、つまりは似ている概念を同じ記号を乱用して使ってる、位に捉えてください。

#命題（Cantor-Bernstein）
$A,B$ を集合として

A \stackrel{f}{\leq} B, B \stackrel{g}{\leq} A \Rightarrow A \stackrel{h}{\equiv} B.

#説明
さて、ここからどっさり説明がいりますね、でもその前に。
$A$と$B$が集合であることを忘れて、数だと思って、しかも何やら不思議な$f,g,h$も忘れるとどうでしょう？当たり前の式に見えませんか？
"数”AとBを比較して互いに相手より等しいか大きい時は、実は両者は等しいということですね。

問題は主役が集合論であり、出てきている演算子諸君がよく知られている大なり小なり記号とはやや異なるということです。

ここで集合論はZFC（選択公理要るんだったかな、、、）の素朴な理解を仮定しています¹、集合とは、元（要素）とは、全射単射など聞いたことがあれば大丈夫だと思います、ま、説明しますが。
あと量化子$\forall, \exists$あと$\exists!$も素朴に使っています。
和集合の記号 $\cup$ や集合の差 $\backslash$ も使っています、が後者は書き下しているのでご安心を。

##演算子のオーバーロード

まず一発目から難題です、いわゆる notation abuse あるいは演算子のオーバーロードに対応している以下の記法

A \stackrel{f}{\leq} B

を説明します。

まずは演算子のオーバーロードについて。
例えば集合同士が等しいかそうでないかを判定する"演算子”

equal.hs

(=) :: Set -> Set -> Bool

の実装は外延性公理を用いて、（任意の）元同士の等値性を比較する普通の

equal.hs

(=) :: Element -> Element -> Bool

でもって実装されています。
すなわち集合の元を一つ一つ比較していって全部等しければ、集合自体も等しいとしましょう、ということです、つまり$A,B$を集合として

(\forall a \in A \Leftrightarrow a \in B) \Rightarrow A = B.

ここでは暗に隠れていますが、括弧の中の”２つの”$a$を比較するのに

equal.hs

(=) :: Element -> Element -> Bool

が使われています。

##包含
さて、集合に”乱用”されてる大なり小なり記号、何かに似てませんか？そう、包含関係です。

X \subseteq Y :\Leftrightarrow (\forall x \in X \Rightarrow x \in Y)

これは包含写像

X \stackrel{i}{\subseteq} Y; x \mapsto i(x) := x

を使えば更に似ているような気がしませんか？

##全射と単射
似ている記号は似ている概念を実装しようと試みた結果だ、と思いましょう。

さて、等号が入った大なり小なりも似たような感じで実装されているわけです、ここでそう！全射と単射が出てくるわけです、ちなみに私はいつも名前がごっちゃるので毎度馬鹿正直に定義を参照して名前で余り呼ばないので未だにどっちがどっちか、、、

（全射）写像 $f:X \to Y$に対して

\forall x \in X, \exists y \in Y \text{ s.t. } b = f(x)

なら全射と呼びます。
先ほど述べた包含を使えばお手軽に書けます、つまり $f$ が全射というのは

f(X) \subseteq Y

ということです。²

（単射）写像 $f:X \to Y$に対して

\forall x \neq x' (\in X) \Rightarrow f(x) \neq f(x') (\in Y)

なら単射と呼びます。

２つが組み合わさると全単射と呼ばれ、全射性から$y$の存在性が、単射性からそのような$y$の唯一性が示せて

\forall x \in X, \exists! y \in Y \text{ s.t. } b = f(x)

となります。
このとき

X \equiv Y \text{ or } X \stackrel{f}{\equiv} Y

と書いて、これを同型と呼びます、平たく言うと一対一に対応する辞書$f: X \to Y$があるよということです。
ここで$\exists!$は存在しかつそれが唯一であるという量化子です。

##包含写像は単射
包含写像は単射であることが簡単に示せます、本質的に等しいかどうかの判定は済んでるのである意味自明ですが。

X \stackrel{i}{\subseteq} Y; x \mapsto i(x) := x \\
x\neq x' \Rightarrow i(x) = x \neq x' = i(x') \in Y.

さてさて、包含 $X \subseteq Y$ の場合は $X$ の要素は本質的に $Y$の要素なわけですが、この条件を緩めることを考えます。
wiki単射に例が載っていますが、まぁそのまま使いましょう、すなわち単射を拡張された包含と考えるわけです。

そしてここで集合の間の $\leq$ を次のように定義します。

A \stackrel{}{\leq} B :\Leftrightarrow (\exists f:A\to B \text{ s.t. } \forall a \neq a' \in A \Rightarrow f(a) \neq f(a') \in B)

すなわち

A \stackrel{}{\leq} B :\Leftrightarrow (\exists f:A\to B \text{ 単射})

そしてこのとき

A \stackrel{f}{\leq} B

と書きます。
単射の存在性だけが大事なときには $f$ すら省くこともあります、おそろしや、、、

##まとめると
集合 $A,B$ に対して

A \stackrel{f}{\leq} B

とは $f:A \to B$ なる単射がありますよ、ということです。
単射が拡張された包含とみなせるので $\subseteq$ と似た記号を"乱用”しているわけです。

#証明たち

##その前に
この証明を取り上げたのは同型を示すのに単射で挟んだら良いというのが魅力的だったからです。
すなわちよくある同型の証明（以下の証明でも使います）は $A \to B$の向きの全射かつ単射なる写像を作るというものなのですが、これを$A \to B$の向きの単射と$B \to A$の向きのこれまた単射を作るでも良いよというのが不思議だったからです。
しかも与えられた $f,g$ から構成的に全単射を構築できるのも不思議な感じがしたのもあります。

##さて、では証明
以下のように再帰的に $A$ の部分集合を定義します。

C_0 := A \backslash g(B) = \left\{ \left. x \right| x \in A \text{ and } x \notin g(B) \right\} \\
C_{n+1} := \{g\circ f (x) | x \in C_n\}, n \geq 0

ここでもし $C_0 = \emptyset$ ならば証明終了です、というのもつまり

C_0 := A \backslash g(B) = \emptyset \Leftrightarrow A = g(B)

これは $g$ が全射であることを示しているので、命題で仮定している $g$ が単射であることと合わせると実は $g$ は全単射だったということになります。
したがって $g: B \equiv A$ は同型となり、万事オーケー。

次に $C_0$ が空集合じゃない時を考えます。
ではここで次のような写像を定義します、well-definedかどうかって？あとで考えましょう！

h(x) := f(x) \text{ if } x \in \bigcup_{n \geq 0} C_n \subseteq A, \\
h(x) := g^{-1}(x) \text{ if } x \in A \backslash \bigcup_{n \geq 0} C_n \subseteq A

一つ目は良いのですが、問題は $x \in A \backslash \bigcup_{n \geq 0} C_n$ の時の定義ですね。
$C_0$ は$g$ の像³が取り除かれているので、以降の $C_n$ はその定義から $g$ の像は入ってません、したがって $A \backslash \bigcup_{n \geq 0} C_n$ は $g$ の像になっているわけです。
ややこしいですが、 $A$ から $g$ の像でない部分を丁寧に取り除く処置をしているのです、つまるところのところ。
すなわち $\forall x \in A \backslash \bigcup_{n \geq 0} C_n$ に対して少なくとも１つ $b \in B$ があって $g(b) = x$ を満たすわけですが、ここで $g$ の単射性からかくなる $b \in B$ は唯一だということがわかるのでこんな $b$ を

b = g^{-1} (x)

と書いても良いことがわかります。
したがって上記の条件付きな写像 $h$ はwell-defined であることがわかります、安全安全。

##hの単射性
$B$ の部分集合を

D_n := f(C_n) = \{f(x)| x \in C_n\}

で定義すると

C_{n+1} = g(D_n) = \{g(y) | y \in D_n\}

となることがわかります。
$h$ の定義の中の $f$ はもちろん単射ですが、実は $g^{-1}$ の部分も単射になっています：

\forall x,x' \in A \backslash \bigcup_{n \geq 0} C_n,\\
h(x) = h(x') \Rightarrow x = g\circ h(x) = g\circ h(x') = x'

すなわち危険が生じる可能性があるのは比較するべき元がそれぞれ $\bigcup_{n \geq 0} C_n$ と $A \backslash \bigcup_{n \geq 0} C_n$ に分かれている時になります。
この時 $x \neq x'$ をそれぞれ

x \in C_m, h(x) = f(x) \in D_m

と

x' \notin \bigcup_{n \geq 0} C_n, h(x') = g^{-1}(x')

とします、この時

h(x') = g^{-1}(x') \notin D_m \\
h(x) = f(x) \in D_m

となります。
この $h(x)$ と $h(x')$ は住んでる集合が違うので、$h(x) \neq h(x')$ となります。
まとめるといずれのケースでも

x \neq x' \Rightarrow h(x) \neq h(x')

となって $h$ が単射であることが示せました。

##全射性
$\forall y \in B$ を考えます。
この $y$ に行くような $A$ の元が見つかれば良いというわけです。
すなわち $y$ が $h$ の像 $h(A)$ の中に入ってることを示せば良いことになります。

$y$ は

y \in \bigcup_{n \geq 0} D_n

かあるいは

y \in B \backslash \bigcup_{n \geq 0} D_n

の場合分けになります。
前者のケース $y \in \bigcup_{n \geq 0} D_n$ ならば

\bigcup_{n \geq 0} D_n = \bigcup_{n \geq 0} f(C_n) = f\left(\bigcup_{n \geq 0} C_n \right) \subseteq f(A)

となるので⁴、$y \in h(A)$ が分かります、したがってこのケースの場合は全射であることが示せました。

後者のケース $y \in B \backslash \bigcup_{n \geq 0} D_n = B \backslash \bigcup_{n \geq 0} f(C_n) $ ならば

g(y) \notin C_0

が分かります。
また $C_{n+1} = g(D_n)$ から

g(y) \notin C_n, \forall n \geq 0

であることも分かります。
従って

g(y) \in A \backslash \bigcup_{n \geq 0} C_n

であり、このとき

h\circ g (y) = g^{-1} \circ g (y) = y.

となりますが、これはすなわち

y \in h (A)

ということが分かりました、つまり後者のケースでも $h$ は全射であることが分かりました。
よって$h$は全射であることが示せました。

##結論
以上のように作った $h: A \to B$ が全単射であることがわかったので $A,B$ は同型であることが分かります。
すなわち

A \stackrel{h}{\equiv} B.

再掲すると

A \stackrel{f}{\leq} B, B \stackrel{g}{\leq} A \Rightarrow A \stackrel{h}{\equiv} B.

となります。

#あとがき

これはもともと人間の脳コンパイラがいかに賢いか（構文解析能力の高さと演算子、関数のオーバーロードを文脈などから型推論してこなす）を議論してた時に思い出した命題でした。
もともと圏論的な矢印や集合論を勉強してた時に見つけた面白そうな証明で、オリジナルはこちらです。
今年の手帳とさよならする前に見つけたのでこちらに書かせていただきました。
読んでくださった型、間違った、読んでくださった方々ありがとうございました、感想コメント訂正等気軽によろしくお願いします。

ここがここが元ネタですが、選択公理はいらないそうです。(http://alg-d.com/math/ac/bernstein.html) ↩
ここでは関数、あるいは写像のオーバーロードが行われています、すなわち $f(X) := {f(x) | x \in A} \subseteq B$ なる集合です。 ↩
$g:B \to A$ の像とは $A$ の部分集合である $g(B)$ のことです。 ↩
真ん中の等号は以下のように示せます。$f(C\cup C') = \{y | \exists x \in C\cup C', y = f(x) \} = \{ y | \exists x \in C \text{ or } x \in C', y = f(x) \} = \{y | f(x) \in f(C) \text{ or } f(x) \in f(B), y = f(x) \} = f(A) \cup f(B) $ ↩