対
word(ss,s)! …【\(\langle {\sf X} , {\sf Y} \rangle\)】対の定義はされません。次のものは対の成分を取り出します。
word(s,s) … \({\rfloor}\) \({\lfloor}\)
\({\rfloor.}\)【\({\rfloor} \langle x , y \rangle = x\)】
\({\lfloor.}\)【\({\lfloor} \langle x , y \rangle = y\)】
\(\text{%0}\)【\(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\)】\(\) ◀ \({\rfloor.}\,{\bf ,}\,{\lfloor.}\)
直積、関係
word(cc,c) … \(\times\)def …【\({\sf C} \times {\sf D}\)】≃【\(\{ \langle {\sf x} , {\sf y} \rangle \mid {\sf x} \in {\sf C} , {\sf y} \in {\sf D} \}\)】
word(ss,s) … \(\times\)
\(\times.\)【\(X \times Y = X \times Y\)】
\(\text{Set}^2\)【\(\widehat{\times} \text{Set} = \{ x \mid x = \langle {\rfloor} x , {\lfloor} x \rangle \} \)】\(\) ◀ \({\rfloor.}\,{\bf ,}\,{\lfloor.}\)
対の集まりは関係とよばれます。
word(,c) … \(\text{Rel}\)
def …【\(\text{Rel}\)】≃【\(\{ R \mid R \subset \widehat{\times} \text{Set} \} \)】
abbr …【\(\langle {\sf p} \rangle\)】≈【\(\{ \langle {\sf x} , {\sf y} \rangle \mid {\sf x} \, {\sf p} \, {\sf y} \}\)】
word(ss,p)と関係は等価です。\({\sf X} {\sf p} {\sf Y} \Longleftrightarrow \langle {\sf X} , {\sf Y} \rangle \in \langle {\sf p} \rangle\)
word(,c) … \(\text{Id}\)
def …【\(\text{Id}\)】≃【\(\{ \langle x , x \rangle \mid x \in \text{Set} \}\)】
\(\text{Id0}\)【\(\text{Id} = \langle = \rangle\)】\(\) ◀ O
定義域、値域
word(c,c)F … \(\text{dom}\) \(\text{rng}\)def …【\(\text{dom} ( {\sf R} )\)】≃【\(\{ {\sf x} \mid \exists {\sf y} \, \langle {\sf x} , {\sf y} \rangle \in {\sf R} \} \)】
def …【\(\text{rng} ( {\sf R} )\)】≃【\(\{ {\sf y} \mid \exists {\sf x} \, \langle {\sf x} , {\sf y} \rangle \in {\sf R} \} \)】
word(s,s)F … \(\text{dom}\) \(\text{rng}\)
\(\text{dom.}\)【\(\text{dom} ( R ) = \text{dom} ( R )\)】
\(\text{rng.}\)【\(\text{rng} ( R ) = \text{rng} ( R )\)】
\(\text{Rel0}\)【\(R \in \text{Rel} \Longrightarrow R \subset \text{dom} ( R ) \times \text{rng} ( R )\)】\({\bf /}{\subset.}{\bf /}\times.{\bf /}\text{dom.}{\bf /}\text{rng.}\) ◀ O
成分の入れ替え
word(s,s) … \(^\leftrightarrow\)\(\text{sw.}\)【\(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)】
word(c,c) … \(^\leftrightarrow\)
def …【\({\sf R} ^\leftrightarrow\)】≃【\(\{ {\sf p} ^\leftrightarrow \mid {\sf p} \in {\sf R} \}\)】
word(s,s) … \(^\leftrightarrow\)
\(\text{Psw.}\)【\({\sf R} ^\leftrightarrow = {\sf R} ^\leftrightarrow\)】
合成
word(cc,c) … \(\circ\)def …【\({\sf S} \circ {\sf R}\)】≃【\(\{ \langle {\sf x} , {\sf z} \rangle \mid \exists {\sf y} \, ( \langle {\sf x} , {\sf y} \rangle \in {\sf R} , \langle {\sf y} , {\sf z} \rangle \in {\sf S} ) \}\)】
\({\circ}左単\)【\(R \in \text{Rel} \Longrightarrow \text{Id} \circ R = R\)】\(\) ◀ \(\text{%0}\)
\({\circ}右単\)【\(R \in \text{Rel} \Longrightarrow R \circ \text{Id} = R\)】\(\) ◀ \(\text{%0}\)
\({\circ}単\)【\(R \in \text{Rel} \Longrightarrow \text{Id} \circ R = R = R \circ \text{Id}\)】\(\) ◀ \(\text{%0}\)
&で分けないと時間over
word(ss,s) … \(\circ\)
\({\circ}.\)【\(S \circ R = S \circ R\)】
\({\circ}\text{Rel}\)【\(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\)】\({\bf /}{\subset.}{\bf /}{\circ}.{\bf /}\times.\) ◀ \(\text{%0}\)
\({\circ}結 \)【\(R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R \subset T \circ ( S \circ R )\)】\({\bf /}{\subset.}{\bf /}{\circ}.{\bf /}{\circ}.\) ◀ \(\text{%0}\)
\(\subset\)を\(=\)にすると時間over