Schröder–Bernsteinの定理

単射と濃度を論じる上で非常に基礎的な定理

簡単な説明

$ |A|\le|B|\land|A|\ge|B|\implies|A|=|B|

これで一見証明が済んでいるように思われるが、濃度の大小関係や等号を定義するのにSchröder–Bernsteinの定理が必要なので、証明にはなっていない

Schröder–Bernsteinの定理を同値変形した論理式、とは言えるかもtakker.icon

これも証明はまだ書いてないが

厳密な論理式

$ \forall A, B;\left[\begin{cases}\exists f:A\rightarrowtail B\\\exists f:B\rightarrowtail A\end{cases}\implies\exists f:A⤖ B\right]

各方向への単射があるなら、全単射が存在する

Reference

証明Schröder–Bernsteinの定理#660f85021280f00000eb2d92

$ \forall A\forall Bにて

$ \exist f:A\rightarrowtail B\exist g:B\rightarrowtail A

ここで次を定義する

$ C:\Z_{\ge0}\ni n\mapsto\begin{dcases}A\setminus g[B]&\text{if }n=0\\g\circ f[C(n-1)]&\text{otherwise}\end{dcases}\in A

$ C:=\bigcup_{n\in\Z_{\ge0}} C(n)

$ g':B\ni y\mapsto g(y)\in g[B]

$ gを全単射にしたもの

$ h:A\ni x\mapsto\begin{dcases}f(x)&\text{if }x\in C\\{g'}^{-1}(x)&\text{otherwise}\end{dcases}\in B

この条件のもと、$ hが全単射であることを示す

単射性

$ \forall a_1,a_2\in A;

$ h(a_1)=h(a_2)

$ \implies\begin{dcases}a_1=a_2&\text{if }a_1,a_2\in C\lor a_1,a_2\notin C\\f(a_1)={g'}^{-1}(a_2)&\text{if }a_1\in C\land a_2\notin C\\{g'}^{-1}(a_1)=f(a_2)&\text{if }a_1\notin C\land a_2\in C\end{dcases}

1番目の条件は$ f,g'の単射性から導かれた

2,3番目は$ hの定義を適用した

$ \iff\begin{dcases}a_1=a_2&\text{if }a_1,a_2\in C\lor a_1,a_2\notin C\\{g'}\circ f(a_1)=a_2&\text{if }a_1\in C\land a_2\notin C\\a_1={g'}\circ f(a_2)&\text{if }a_1\notin C\land a_2\in C\end{dcases}

$ \iff\begin{dcases}a_1=a_2&\text{if }a_1,a_2\in C\lor a_1,a_2\notin C\\{g'}\circ f(a_1)=a_2\land\exist n\in\N;a_1\in C(n-1)&\text{if }a_1\in C\land a_2\notin C\\a_1={g'}\circ f(a_2)\land\exist n\in\N;a_2\in C(n-1)&\text{if }a_1\notin C\land a_2\in C\end{dcases}

$ a_1\in C,a_2\in Cを$ Cの定義で展開しただけ

$ \implies\begin{dcases}a_1=a_2&\text{if }a_1,a_2\in C\lor a_1,a_2\notin C\\\exist n\in\N\exist a'\in C(n-1);a_2=g\circ f(a')&\text{if }a_1\in C\land a_2\notin C\\\exist n\in\N\exist a'\in C(n-1);a_1=g\circ f(a')&\text{if }a_1\notin C\land a_2\in C\end{dcases}

∃導入で$ a'を導入

$ \implies\begin{dcases}a_1=a_2&\text{if }a_1,a_2\in C\lor a_1,a_2\notin C\\a_2\in C&\text{if }a_1\in C\land a_2\notin C\\a_1\in C&\text{if }a_1\notin C\land a_2\in C\end{dcases}

$ n\ge1 のとき$ g\circ f[C(n-1)] =C(n)\subseteq C であることを使った

$ \implies a_1=a_2

$ a_1=a_2以外は矛盾が生じることを示した

全射性

$ h[A]=B 示す

$ h[A]=f[C]\cup{g'}^{-1}[A\setminus C]

$ =f[C]\cup g^\gets[A\setminus C]

$ g'は全単射なので、逆写像の像と逆像が等しくなる

$ =f[C]\cup(g^\gets[A]\setminus g^\gets[C])

$ =f[C]\cup(B\setminus g^\gets[C])

$ g: B\rightarrowtail A だから$ g^\gets[A]=B

$ =f[C]\cup(B\setminus\{b\in B|g(b)\in C\})