2 列

2.1 列

1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s)F … \(\mathsf{ary}_{\tt n}\)
abbr … \(\langle X_{1} , \cdots , X_{\tt n} \rangle\) ≈ \(\mathsf{ary}_{\tt n} ( X_{1} , \cdots , X_{\tt n} )\)
ary\({\tt n}\). … \(\langle x_{1} , \cdots , x_{\tt n} \rangle = \{ \langle 0 , x_{1} \rangle , \cdots , \langle {\tt n\,{\text -}\,1} , x_{\tt n} \rangle \}\)
ary\({\tt n}\)L … \(f \in {\tt n} \to \mathbb{V} \Rightarrow f = \langle f ( 0 ) , \cdots , f ( {\tt n\,{\text -}\,1} ) \rangle\) \(\blacktriangleleft\) \(\mathbb{W}.\)
ary\({\tt n}\)S … \(\langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \stackrel{\rm S}\to \{ x_{1} , \cdots , x_{\tt n} \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

ary1IS … \(\langle x \rangle \in 1 \stackrel{\rm IS}\to \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
2以上の自然数 \({\tt n}\) に対して
ary\({\tt n}\)IS … \(x_{0} \neq x_{1} , \cdots\!\cdots , x_{\tt n\,{\text -}\,2} \neq x_{\tt n\,{\text -}\,1} \Longleftrightarrow \langle x_{0} , \cdots , x_{\tt n\,{\text -}\,1} \rangle \in {\tt n} \stackrel{\rm IS}\to \{ x_{0} , \cdots , x_{\tt n\,{\text -}\,1} \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.2 自然数と濃度

=#1 … \(X \stackrel{\#}= 1 \Longleftrightarrow \exists x \, X = \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
2以上の自然数 \({\tt n}\) に対し
=#\({\tt n}\) … \(X \stackrel{\#}= {\tt n} \Longleftrightarrow \exists^* x_{1} , \cdots , x_{\tt n} ( X = \{ x_{1} , \cdots , x_{\tt n} \} )\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=#℘ … \(\wp X \stackrel{\#}= X \to 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s

2.3 有限個の直積

word(s\(^{\tt n}\),s)F … \(\times_{{\tt n}}\)
abbr … \(X_{1} \times \cdots \times X_{\tt n}\) ≈ \(\times_{{\tt n}} ( X_{1} , \cdots , X_{\tt n} )\)
×\({\tt n}\). … \(X_{1} \times \cdots \times X_{\tt n} = \{ \langle x_{1} , \cdots , x_{\tt n} \rangle \mid x_{1} \in X_{1} , \cdots , x_{\tt n} \in X_{\tt n} \}\)
×\({\tt n}\).. … \(X_{1} \times \cdots \times X_{\tt n} = \{ f \in {\tt n} \to \mathbb{V} \mid f ( 0 ) \in X_{1} , \cdots , f ( {\tt n\,{\text -}\,1} ) \in X_{\tt n} \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
×\({\tt n}\)! … \(X_{1} = X , \cdots , X_{\tt n} = X \Longrightarrow X_{1} \times \cdots \times X_{\tt n} = {\tt n} \to X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.4 互換

word(ss,s) … \(\leftrightharpoons\)
exc. … \(x \leftrightharpoons y = \{ \langle x , y \rangle , \langle y , x \rangle \}\)