集合・写像・個数（=#）を準備する。

1 集合

1.1 基本的な集合関数

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

word(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)

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 \mid x \in X , x \in Y \}\)
∖. … \(X \mathop\setminus Y = \{ x \in X \mid x \notin Y \}\)
word(c,s) … \(\)
set_. … \(\dot\exists C \Longrightarrow C = C\)
word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)

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(s,s) … \(^{\hat\leftrightarrow}\)
^sw. … \(R ^{\hat\leftrightarrow} = \{ \langle y , x \rangle \mid \langle x , y \rangle \in R \}\)
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)F … \({\hat\triangleleft}\)
^◁. … \({\hat\triangleleft} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)

1.3 写像、全単射

word(ss,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 \}\)
∅→ … \(\emptyset \to X = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→IS. … \(X \stackrel{\rm IS}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists! x \, \langle x , y \rangle \in f \}\)
→IS^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^{\hat\leftrightarrow} \in Y \stackrel{\rm IS}\to X\) \(\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}.\)
→IS∪ … \(\begin{cases} f \in X \stackrel{\rm IS}\to X' \\ g \in Y \stackrel{\rm IS}\to Y' \end{cases} , \begin{cases} X \cap Y = \emptyset \\ X' \cap Y' = \emptyset \end{cases} \Longrightarrow f \cup g \in X \cup Y \stackrel{\rm IS}\to X' \cup Y'\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(s,s) … \(\text{id}\)
id. … \(\text{id} _ X = \{ \langle x , x \rangle \mid x \in X \}\)
id:0 … \(\text{id} _ X \in X \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,p) … \(\stackrel{\#}=\)
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)
=#:R … \(X \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#:T … \(X \stackrel{\#}= Y \stackrel{\#}= Z \Longrightarrow X \stackrel{\#}= Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#:X … \(X \stackrel{\#}= Y \Longleftrightarrow Y \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#∅ … \(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#∪ … \(\begin{cases} X \stackrel{\#}= X' \\ Y \stackrel{\#}= Y' \end{cases} , \begin{cases} X \cap Y = \emptyset \\ X' \cap Y' = \emptyset \end{cases} \Longrightarrow X \cup Y \stackrel{\#}= X' \cup Y'\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.4 補題

元が同じ集合は等しい。
Lext … \(\forall p \, ( p \in X \Longleftrightarrow p \in Y ) \Longrightarrow X = Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
どの集合にも、その元でないものがある。
Lout … \(\exists x \, x \notin X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
1点ずつ足しても個数の等しさは保たれる。
=#∪1 … \(X \stackrel{\#}= Y , a \notin X , b \notin Y \Longrightarrow X \cup \{ a \} \stackrel{\#}= Y \cup \{ b \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
1点を足して取り除くと元に戻り、1点を取り除いて足しても元に戻る。
∈∪1 … \(x \in X \cup \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∪∖1 … \(x \notin X \Longrightarrow ( X \cup \{ x \} ) \mathop\setminus \{ x \} = X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
∖∪1 … \(x \in X \Longrightarrow X = ( X \mathop\setminus \{ x \} ) \cup \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
1点ずつ取り除いても個数の等しさは保たれる。
=#∖1 … \(X \stackrel{\#}= Y , a \in X , b \in Y \Longrightarrow X \mathop\setminus \{ a \} \stackrel{\#}= Y \mathop\setminus \{ b \}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
L×1 … \(X \times \{ c \} \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
L×0 … \(X \times \emptyset = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
個数の等しい集合どうしの直積は、個数が等しい。
=#× … \(X \stackrel{\#}= X' , Y \stackrel{\#}= Y' \Longrightarrow X \times Y \stackrel{\#}= X' \times Y'\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
個数の等しい集合からの写像の集合は、個数が等しい。\(u \mapsto u \circ h^{-1}\) が全単射になる。
→=# … \(X \stackrel{\#}= X' \Longrightarrow X \to Y \stackrel{\#}= X' \to Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
1点との直積は、もとの集合と個数が等しい。
L1× … \(\{ c \} \times X \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s