3 集合の大きさ比較

3.1 単射、全射、全単射

word(ss,s) … \(\stackrel{\rm I}\to\)  \(\stackrel{\rm S}\to\)  \(\stackrel{\rm IS}\to\)
→I. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^{\hat\leftrightarrow} \in {\hat\triangleright} ( f ) \to \mathbb{V} \}\)
→S. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to \mathbb{V} \mid {\hat\triangleright} ( f ) = Y \}\)
→I.. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall^* x_{0} , x_{1} \in X . f ( x_{0} ) \neq f ( x_{1} ) \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→S.. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \in X . y = f ( x ) \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→S:0 … \(f \in X \to \mathbb{V} \Longrightarrow f \in X \stackrel{\rm S}\to {\hat\triangleright} ( f )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→IS. … \(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)
→IS^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^{\hat\leftrightarrow} \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

→I∘ … \(f \in X \stackrel{\rm I}\to Y , g \in Y \stackrel{\rm I}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm I}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→S∘ … \(f \in X \stackrel{\rm S}\to Y , g \in Y \stackrel{\rm S}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm S}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→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}.\)

3.2 恒等写像

word(s,s) … \(\text{id}\)
id. … \(\text{id} _ X = \lceil \bullet \rfloor | _ X\)
id:0 … \(\text{id} _ X \in X \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∘E … \(R \subset X \times Y \Longrightarrow R \circ \text{id} _ X = R = \text{id} _ Y \circ R\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(R \in \text{Rel} \Longrightarrow R | _ X = R \circ \text{id} _ X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→I... … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^{\hat\leftrightarrow} \circ f = \text{id} _ X \} = \{ f \in X \to Y \mid \exists g \, g \circ f = \text{id} _ X \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→S... … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid f \circ f ^{\hat\leftrightarrow} = \text{id} _ Y \} = \{ f \in X \to Y \mid \exists g \, f \circ g = \text{id} _ Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \neq \emptyset \Longrightarrow X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \exists g \in Y \to X . g \circ f = \text{id} _ X \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

3.3 濃度

word(ss,p) … \(\stackrel{\#}=\)  \(\stackrel{\#}\le\)  \(\stackrel{\#}<\)
=#. … \(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\)
<#. … \(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \stackrel{{\tt /}}{\stackrel{\#}=} Y\)
=#:RTX … \([\stackrel{\#}=] :\mathsf{R}\mathsf{T}\mathsf{X}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
≤#:RT … \([\stackrel{\#}\le] :\mathsf{R}\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
sub_≤# … \([\subset] \stackrel{\star\!\star}{\Rightarrow} [\stackrel{\#}\le]\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#0 … \(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
CSB … \(X \stackrel{\#}\le Y \stackrel{\#}\le X \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
単調写像の不動点（KT）を使っても示せます。
\(X \stackrel{\#}\le Y \stackrel{\#}\le X \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
\(X \stackrel{\#}< \wp X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

3.4 選択公理

word(s,s)F … \(\text{choice}\)
choice. … \(\text{choice} ( \mathcal{X} ) = \{ f \in \mathcal{X} \to \mathbb{V} \mid \forall X \in \mathcal{X} . f ( X ) \in X \}\)
\(X = \{ x \} \Longrightarrow \text{choice} ( \{ X \} ) = \{ \{ \langle X , x \rangle \} \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\emptyset \in \mathcal{X} \Longrightarrow \text{choice} ( \mathcal{X} ) = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
ax_c … \(\forall \mathcal{X} \not\ni \emptyset . \text{choice} ( \mathcal{X} ) \neq \emptyset\)
ACRI … ax_c \(\Longleftrightarrow \forall X , Y \, X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \exists g \in Y \to X . f \circ g = \text{id} _ Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

3.5 直積

word(s,s) … \(\Pi\)
∏. … \(X \in \Lambda \to \mathbb{V} \Longrightarrow \Pi X = \{ x \in \Lambda \to \mathbb{V} \mid \forall \lambda \in \Lambda . x _ \lambda \in X _ \lambda \}\)
\(X \in \Lambda \to \mathbb{V} , \emptyset \in {\hat\triangleright} ( X ) \Longrightarrow \Pi X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
Dp_c … \(X \in \Lambda \to \mathbb{V} , \emptyset \notin {\hat\triangleright} ( X ) \Longrightarrow \Pi X \neq \emptyset\)