1 - c

c1

対も基本的です。
ここでも定義は与えられません。\(\langle x,y\rangle=\{x,\{x,y\}\}\) とはしません。

対、直積

word(ss,s)F … pr　　abbr …【\(\langle x , y \rangle\)】≈ pr ($x , $y)
次のものは対の成分を取り出します。
word(s,s) … \(\triangleleft\)  \(\triangleright\)  
pr<.【\(\triangleleft \langle x , y \rangle = x\)】
pr>.【\(\triangleright \langle x , y \rangle = y\)】
pr0【\(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\)】\(\blacktriangleleft\)

word(ss,s) … \(\times\)  
\({\times}.\) {pr_ **=_ #Ppr}
対の集合(直積の部分集合)は関係と呼ばれます。
word(,c) … \(\text{Rel}\)  
cvt …【\(\text{Rel}\)】≃【\(\{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\)】

定義域、値域

word(s,s)F … \(\text{dom}\)  \(\text{im}\)  
dom.【\(\text{dom} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)】
im.【\(\text{im} ( R ) = \{ y \mid \exists x \, \langle x , y \rangle \in R \}\)】
【\(\text{Rel} = \{ R \mid R \subset \text{dom} ( R ) \times \text{im} ( R ) \}\)】\(\blacktriangleleft\)

定義域の制限や像は写像に対してよく使用されます。
word(ss,s) … \(|\)  
rest.【\(R | _ X = \{ \langle x , y \rangle \in R \mid x \in X \}\)】
word(ss,s) … ap_  
ap_.【\(R ( A ) = \{ y \mid \exists a \in A . \langle a , y \rangle \in R \}\)】

代入

word(s,s) … \(\text{dom!}\)  
dom!.【\(\text{dom!} ( f ) = \{ x \mid \exists! y \, \langle x , y \rangle \in f \}\)】

=% ≅ =
word(ss,s)F … ap  
=%.【\(x \in \text{dom!} ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)】
ap0【\(x \in \text{dom!} ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\)】\(\blacktriangleleft\)
ap_0【\(A \subset \text{dom!} ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\)】\(\blacktriangleleft\)

成分の入れ替え

word(s,s) … \(^\leftrightarrow\)  
sw.【\(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)】
sw巾【\(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\)】\(\blacktriangleleft\)

word(s,s) … \(^\leftrightarrow\)  
sw_.【\(^\leftrightarrow \,^{\star\!\star}{=}\; {^\leftrightarrow}\)】
sw_0【\(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\)】\(\blacktriangleleft\)
sw_巾【\(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\)】\(\blacktriangleleft\)

合成

word(ss,s) … \(\circ\)  
comp.【\(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)】
compRel【\(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\)】\(\blacktriangleleft\)
comp_A【\( R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\)】\(\blacktriangleleft\)
comp逆【\( R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\)】\(\blacktriangleleft\)
comp_ap【\(x \in \text{dom!} ( f ) , f ( x ) \in \text{dom!} ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\)】\(\blacktriangleleft\)

c2

写像とは「集合の各元をそれぞれ対応させるもの」です。
当システムでは写像は特別な関係として定義されます。

写像

word(ss,s) … \(\to\)  
->.【\(X \to Y = \{ f \subset X \times Y \mid X \subset \text{dom!} ( f ) \}\)】
【\(f \in \text{dom} ( f ) \to \text{im} ( f ) \Longleftrightarrow f \in \text{Rel} , \text{dom} ( f ) = \text{dom!} ( f )\)】\(\blacktriangleleft\)

【\(\emptyset \to X = \{ \emptyset \}\)】\(\blacktriangleleft\)
【\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\)】\(\blacktriangleleft\)
->comp【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\)】\(\blacktriangleleft\)
->rest【\(f \in X \to Y \Longrightarrow f | _ A \in X \cap A \to Y\)】\(\blacktriangleleft\)

アロー関数

word(vss,s) … fn　　abbr* …【\([ x \mapsto X ]\)】≈ fn $x ($X)
cvt … 【\([ x \mapsto X ] \, T\)】≃【\(X^{x\,\mapsto\,T}\)】
【\([ x \mapsto X ]\)】は一項関数と思えます。

第一引数を略して \(\bullet\) にできます。\(\mapsto\) も略されます。例　【\([ \bullet + a ]\)】≈【\([ x \mapsto x + a ]\)】
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例　【\([ \bullet + [ \bullet + x ] y ]\)】≃【\([ \bullet + ( y + x ) ]\)】

一項関数の制限

一項関数の制限により写像が作られます。ただしクラスであることに注意。
abbr …【\( \mathop{{\sf f}} _ X\)】≈【\(\{ \langle x , \mathop{{\sf f}} x \rangle \mid x \in X \}\)】

word(s,c) … \(\text{Map}\)  
cvt …【\(\text{Map} ( X )\)】≃【\(\{ f \mid f = [ f ( \bullet ) ] _ X \}\)】
->.._【\(X \to Y = \{ f \in \text{Map} ( X ) \mid \text{im} ( f ) \subset Y \}\)】\(\blacktriangleleft\)
【\(\text{Map} ( X ) = \{ f \mid \exists Y \, f \in X \to Y \}\)】\(\blacktriangleleft\)
【\( f , g \in \text{Map} ( X ) \Longrightarrow f = g \Leftrightarrow \forall x \, f ( x ) = g ( x )\)】\(\blacktriangleleft\)

一点集合と写像

word(ss,s) … \(|\)  
on.【\(y | _ X = [ x \mapsto y ] _ X\)】
【\(y | _ X = X \times \{ y \}\)】\(\blacktriangleleft\)
on0【\(X \to \{ y \} = \{ y | _ X \}\)】\(\blacktriangleleft\)

【\(\{ x \} \to Y = \{ \{ \langle x , y \rangle \} \mid y \in Y \}\)】\(\blacktriangleleft\)

c3

単射、全射

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 ^\leftrightarrow \in \text{im} ( f ) \to X \}\)】
->S._【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{im} ( f ) = Y \}\)】
->IS.【\(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)】
->IS..【\(X \stackrel{\rm IS}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in Y \to X \}\)】\(\blacktriangleleft\)
->IS.. / ->IS. [/ ->I._ / ->S._ => ＜ O || <= // W. ＜ sw.] の方が良い証明
->ISsw_【\(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^\leftrightarrow \in Y \stackrel{\rm IS}\to X\)】\(\blacktriangleleft\)

->Icomp【\(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\)
示せなくなった。->I. 変更のせい？
->Scomp【\(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\)
->IScomp【\(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\)

恒等写像

word(s,s) … \(\text{id}\)  
id.【\(\text{id} _ X = [ \bullet ] _ X\)】
id0【\(\text{id} _ X \in X \stackrel{\rm IS}\to X\)】\(\blacktriangleleft\)
comp単【\(R \subset X \times Y \Longrightarrow \text{id} _ Y \circ R = R = R \circ \text{id} _ X\)】\(\blacktriangleleft\)
【\(R \in \text{Rel} \Longrightarrow R | _ X = R \circ \text{id} _ X\)】\(\blacktriangleleft\)

【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \circ f = \text{id} _ X \} = \{ f \in X \to Y \mid \exists g \, g \circ f = \text{id} _ X \}\)】\(\blacktriangleleft\)
【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid f \circ f ^\leftrightarrow = \text{id} _ Y \} = \{ f \in X \to Y \mid \exists g \, f \circ g = \text{id} _ Y \}\)】\(\blacktriangleleft\)

列

1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s)F … ary\({\tt n}\)　　abbr …【\(\langle x_{1} , \cdots , x_{\tt n} \rangle\)】≈ ary\({\tt n}\) ($x1 , … , $xn)
例　【\(\langle x , \langle x , y \rangle \rangle\)】≈ ary2 (x , ary2 (x , y))
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}\)0【\(f \in \text{Map} ( {\tt n} ) \Longrightarrow f = \langle f ( 0 ) , \cdots , f ( {\tt n\,{\text -}\,1} ) \rangle\)】
ary1IS【\(\langle x \rangle \in 1 \stackrel{\rm IS}\to \{ x \}\)】\(\blacktriangleleft\)

2以上の自然数 \({\tt n}\) に対して
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\)
ary3S // W. [&l // !OA ＜ neq3 ,, pr0 || &r ＜ O] なぜか時間かかる
ary3S // W. [&l [&l ＜ O || &r // !OA ＜ neq3 ,, pr0] || &r ＜ O]
ary\({\tt n}\)IS【\(x_{1} \neq x_{2} , \cdots \Longleftrightarrow \langle x_{1} , \cdots , x_{\tt n} \rangle \in {\tt n} \stackrel{\rm IS}\to \{ x_{1} , \cdots , x_{\tt n} \}\)】\(\blacktriangleleft\)
ary3IS / ->IS. => &l / ->I. &l ＜ ary3S / ->S.　〇
ary3IS / ->IS. => &l / ->I. &r / W. ＜ neq3 ,, pr0　〇
ary3IS / ->IS. => &l / ->I. &r / set3.x / W. ＜ neq3 ,, pr0　〇
ary3IS / ->IS. => &l / ->I. &r / W. // !OA ＜ neq3 ,, pr0　✖
ary3IS / ->IS. => &l / ->I. &r / W. /22 !OA /221 !OA ＜ neq3 ,, pr0 ＜ O　〇
ary3IS / ->IS. => &r ＜ ary3S
ary4IS // W. <= ＜ neq4

選択写像

word(s,s)F … \(\text{choice}\)  
choice._【\(\text{choice} ( \mathcal{X} ) = \{ f \in \text{Map} ( \mathcal{X} ) \mid \forall X \in \mathcal{X} . f ( X ) \in X \}\)】
【\(X = \{ x \} \Longrightarrow \text{choice} ( \{ X \} ) = \{ \langle X , x \rangle \}\)】\(\blacktriangleleft\)
未完　// W. をしたときに w1 がおかしい
ax_c【\(\emptyset \notin \mathcal{X} \Longrightarrow \text{choice} ( \mathcal{X} ) \neq \emptyset\)】

直積

word(s,s) … \(\Pi\)  
dp.【\(X \in \text{Map} ( \Lambda ) \Longrightarrow \Pi X = \{ x \in \text{Map} ( \Lambda ) \mid \forall \lambda \in \Lambda . x _ \lambda \in X _ \lambda \}\)】
dp0【\(X \in \text{Map} ( \Lambda ) , \emptyset \in \text{im} ( X ) \Longrightarrow \Pi X = \emptyset\)】
dp1【\(X \in \text{Map} ( \Lambda ) , \emptyset \notin \text{im} ( X ) \Longrightarrow \Pi X \neq \emptyset\)】