Schröder–Bernsteinの定理
簡単な説明
|A|\le|B|\land|A|\ge|B|\implies|A|=|B|
これで一見証明が済んでいるように思われるが、濃度の大小関係や等号を定義するのにSchröder–Bernsteinの定理が必要なので、証明にはなっていない
Schröder–Bernsteinの定理を同値変形した論理式、とは言えるかも
これも証明はまだ書いてないが
厳密な論理式
\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
\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\})
=f[C]\cup(B\setminus\{b\in B|g(b)\in A\setminus g[B]\lor\exist n\in\N\exist a\in C(n-1);g\circ f(a)=g(b)\})
Cの定義を展開した
=f[C]\cup(B\setminus\{b\in B|\bot\lor\exist n\in\N\exist a\in C(n-1);g\circ f(a)=g(b)\})
\because A\setminus g[B]=A\setminus A=\varnothing
=f[C]\cup(B\setminus\{b\in B|\exist n\in\N\exist a\in C(n-1);f(a)=b\})
\because gの単射性
=f[C]\cup\left(B\setminus\left\{b\in B|\exist a\in\bigcup_{n\in\Z_{\ge0}}C(n);f(a)=b\right\}\right)
=f[C]\cup\left(B\setminus\left\{b\in B|\exist a\in C;f(a)=b\right\}\right)
C(\bullet)をCでまとめた
=f[C]\cup\left(B\setminus f[C]\right)
=B
\therefore\forall A, B;\left[\begin{dcases}\exists f:A\rightarrowtail B\\\exists f:B\rightarrowtail A\end{dcases}\implies\exists f:A⤖ B\right]
References
ここの証明をベースに一度自分で証明書いたんだけど、忘れちゃった
書いた計算用紙も見つからなかった
証明がある
変換過程を複数のイラストで示してあるので、とてもイメージしやすい
#2024-08-01 12:45:13
#2024-04-05 12:24:37
#2022-03-21 20:58:11
#2021-07-03 10:20:51
#2021-04-10 21:05:53