Not logged in / Log in

articles1/25.book(保存済みの内容) … 編集へ / ファイル一覧へ

Cantor-Schröder-Bernsteinの定理
import /common/word_basis.book

1 準備

1.1 空集合、2項関数

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)

word(ss,s) … \(\cup\)  \(\cap\)  \(\mathop\setminus\)
∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
∩. … \(X \cap Y = \{ x \in X \mid x \in Y \}\)
∖. … \(X \mathop\setminus Y = \{ x \in X \mid x \notin Y \}\)

1.2 順序対、直積

word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
word(s,s) … \(\triangleleft\)  \(\triangleright\)
◁. … \(\triangleleft \langle x , y \rangle = x\)
▷. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,s) … \(\times\)
^^pr. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
word(ss,s) … *^ap
*^ap. … \(R ( A ) = \{ y \mid \exists x \in A . \langle x , y \rangle \in R \}\)
\(R(A)\) は \(A\) の \(R\) による像。主定理の説明では \(R[A]\) と書く。

1.3 写像、集合の大きさ比較

\(X \to Y\) は \(X\) から \(Y\) への写像全体の集合(写像は順序対の集合)。矢印の上の I・S・IS は単射・全射・全単射を表す。
word(ss,s) … \(\to\)  \(\stackrel{\rm I}\to\)  \(\stackrel{\rm S}\to\)  \(\stackrel{\rm IS}\to\)
→. … \(X \to Y = \{ f \subset X \times Y \mid \forall x \in X . \exists! y \, \langle x , y \rangle \in f \}\)
→I. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\)
→S. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \, \langle x , y \rangle \in f \}\)
→IS. … \(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)

word(ss,p) … \(\stackrel{\#}=\)  \(\stackrel{\#}\le\)
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)
≤#. … \(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\)

word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)

2 証明①

最小の不動点を作る証明。
単射 \(f : X \to Y\)、\(g : Y \to X\) に対して \(\Phi(B) = (X \setminus g[Y]) \cup g[f[B]]\) とする。
\(\Phi(B) \subset B\) を満たす集合 \(B\) すべてに属する \(X\) の元を集めて \(A\) とする(\(B = X\) が候補の1つ)。
\(\Phi\) は包含を保つ。各候補 \(B\) で \(A \subset B\),\(\Phi(A) \subset \Phi(B) \subset B\) より \(\Phi(A) \subset A\)。
もう一度包含を保つことから \(\Phi(A)\) も候補になり \(A \subset \Phi(A)\)。
よって \(\Phi(A) = A\) で、\(g\) の単射性から \(g(y) \in A \iff y \in f[A]\)。
\(A\) の上では \(f\)、\(X \setminus A\) の上では \(g\) の逆を使って \(f' : X \to Y\) を作る。
\(f'\) は \(A\) を \(f[A]\) へ、\(X \setminus A\) を \(Y \setminus f[A]\) へ全単射に移す。
\(X \stackrel{\#}\le Y \stackrel{\#}\le X \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ,ax_s

3 証明②

word(ss,s) … \(\circ\)
∘. … \(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)
word(s,s) … \(^{\hat\leftrightarrow}\)
^sw. … \(R ^{\hat\leftrightarrow} = \{ \langle y , x \rangle \mid \langle x , y \rangle \in R \}\)
→IS∘ … \(f \in X \stackrel{\rm IS}\to Y , g \in Y \stackrel{\rm IS}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm IS}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→IS^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^{\hat\leftrightarrow} \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

証明①と同じく、閉じた最小の集合を作る証明(Dedekind)。
まず \(X\) をその部分集合 \(Z\) へ単射に移せれば \(X\) と \(Z\) は同じ大きさであることを示す。
単射 \(h : X \to Z\) に対して、\(X \setminus Z\) を含み \(h\) で閉じた最小の集合を \(A\) とする。\(A = (X \setminus Z) \cup h[A]\)。
\(A\) の上では \(h\)、\(X \setminus A\) の上では恒等写像として \(k : X \to Z\) を作ると、\(k\) は全単射になる。
\(Z \subset X , h \in X \stackrel{\rm I}\to Z \Longrightarrow X \stackrel{\#}= Z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ,ax_s

単射 \(f : X \to Y\)、\(g : Y \to X\) があれば、\(g \circ f\) は \(X\) から部分集合 \(g[Y]\) への単射なので \(X\) と \(g[Y]\) は同じ大きさ。
\(g\) は \(Y\) から \(g[Y]\) への全単射なので、合わせて \(X\) と \(Y\) は同じ大きさになる。
\(X \stackrel{\#}\le Y \stackrel{\#}\le X \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ,ax_s

イベント 59 件