対、直積
word(ss,s)! …【\(\langle {\sf X} , {\sf Y} \rangle\)】対の定義はされません。次のものは対の成分を取り出します。
word(s,s) … \(\triangleleft\) \(\triangleright\)
\({\triangleleft.}\)【\(\triangleleft \langle x , y \rangle = x\)】
\({\triangleright.}\)【\(\triangleright \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}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
word(ss,s) … \(\times\)
\({\times}.\) P% := #P%
P%を%_に
定義域、値域
word(s,s)F … \(\text{dom}\) \(\text{im}\)\(\text{dom.}\)【\(\text{dom} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \} \)】
\(\text{im.}\)【\(\text{im} ( R ) = \{ y \mid \exists x \, \langle x , y \rangle \in R \} \)】
定義域の制限や像は写像に対してよく使用されます。
word(ss,s)! …【\({\sf R} | _{ {\sf X} }\)】
\(|.\)【\(R | _{ X } = \{ \langle x , y \rangle \in R \mid x \in X \}\)】
word(ss,s)! …【\({\sf R} ( {\sf A} )\)】
\(\text{Pap}.\)【\(R ( A ) = \{ y \mid \exists a \in A . \langle a , y \rangle \in R \} \)】
成分の入れ替え
word(s,s) … \(^\leftrightarrow\)\(\text{sw.}\)【\(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)】
\(\text{sw}巾\)【\(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
word(s,s) … \(^\leftrightarrow\)
\(\text{sw_.}\)【\(^\leftrightarrow =\!\!= {^\leftrightarrow}\)】
\(\text{sw_0}\)【\(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\text{sw_}巾\)【\(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
Pswをsw_に
合成
word(ss,s) … \(\circ\)\({\circ}.\)【\(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)】
\({\circ}\text{Rel}\)【\(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}結 \)【\(R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}逆\)【\(R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}\text{F}\)【\(( \wp ( \widehat{\times} X ) , \circ ) \, {:}\, \underline{2} \text{A}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
代入
word(s,s) … \(\text{dom!}\)\(\text{dom!}.\)【\(\text{dom!} ( f ) = \{ x \mid \exists! y \, \langle x , y \rangle \in f \} \)】
word(ss,s)! …【\({\sf F} ( {\sf X} )\)】
\(\text{Ap.}\)【\(x \in \text{dom!} ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\)】
\(=\) … =のalias
\({=}.\)【\(x \in \text{dom!} ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\text{PAp0}\)【\(A \subset \text{dom!} ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}\text{Ap}\)【\(x \in \text{dom!} ( f ) , f ( x ) \in \text{dom!} ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(!{\circ}\text{Ap}\)【\(x \in \text{dom!} ( f ) , f ( x ) \in \text{dom!} ( g ) \Longrightarrow x \in \text{dom!} ( g \circ f ) , \langle x , g ( f ( x ) ) \rangle \in g \circ f\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)