3 集合

3.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 \mid x \in X , x \notin Y \}\)
word(cc,c) … \(\cup\)
∪_. … \(A \cup B = \{ x \mid x \in A \mathbin{\rm o\!r} x \in B \}\)

∪∖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 … \(x \in A \mathop\setminus \{ b \} \Longleftrightarrow x \in A , x \neq b\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)

3.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\)  \(\to\)
^^pr. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
→. … \(X \to Y = \{ f \subset X \times Y \mid \forall x \in X . \exists! y \, \langle x , y \rangle \in f \}\)

word(ss,s) … *^ap
*^ap. … \(R ( A ) = \{ y \mid \exists x \in A . \langle x , y \rangle \in R \}\)

3.3 いろいろな写像

word(ss,s) … \(\stackrel{\rm IS}\to\)
→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 \}\)
word(ss,p) … \(\stackrel{\#}=\)
=#. … \(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)
=#∅ … \(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word((s,s)s,s) … \(|\)
Rest. … \(F | _ X = \{ p \mid \exists x \in X . p = \langle x , F ( x ) \rangle \}\)

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}.\)
=#:R … \(X \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(s,s) … \(^{\hat\leftrightarrow}\)
^sw. … \(R ^{\hat\leftrightarrow} = \{ \langle y , x \rangle \mid \langle x , y \rangle \in R \}\)
→IS^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^{\hat\leftrightarrow} \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#:X … \(X \stackrel{\#}= Y \Longleftrightarrow Y \stackrel{\#}= X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

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 ) \}\)
→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}.\)
=#:T … \(X \stackrel{\#}= Y \stackrel{\#}= Z \Longrightarrow X \stackrel{\#}= 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}.\)
→IS∖1 … \(f \in X \stackrel{\rm IS}\to Y , \langle x , y \rangle \in f \Longrightarrow f \mathop\setminus \{ \langle x , y \rangle \} \in X \mathop\setminus \{ x \} \stackrel{\rm IS}\to Y \mathop\setminus \{ y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→IS∪1 … \(f \in X \stackrel{\rm IS}\to Y , x \notin X , y \notin Y \Longrightarrow f \cup \{ \langle x , y \rangle \} \in X \cup \{ x \} \stackrel{\rm IS}\to Y \cup \{ y \}\) \(\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}.\)
=#１ … \(X \stackrel{\#}= \{ a \} \Longleftrightarrow \exists x \, X = \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
個数の等しい集合どうしの直積は、個数が等しい。
=#× … \(X \stackrel{\#}= X' , Y \stackrel{\#}= Y' \Longrightarrow X \times Y \stackrel{\#}= X' \times Y'\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

word(s,s)F … \({\hat\triangleleft}\)
^◁. … \({\hat\triangleleft} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)