合成
word(cc,c) … \(\circ\)def …【\({\sf R} \circ {\sf S}\)】≃【\(\{ \langle {\sf x} , {\sf z} \rangle \mid \exists {\sf y} \, ( \langle {\sf x} , {\sf y} \rangle \in {\sf R} , \langle {\sf x} , {\sf y} \rangle \in {\sf S} ) \}\)】
word(ss,s) … \(\circ\)
\({\circ}.\)【\({\sf R} \circ {\sf S} = {\sf R} \circ {\sf S}\)】
\({\circ}\text{Rel}\)【\(\text{Rel} ( R ) , \text{Rel} ( S ) \Longrightarrow \text{Rel} ( R \circ S )\)】/\({\circ}.\)◀ O
\({\circ}\text{Map}\)【\(\text{Map} ( f ) , \text{Map} ( g ) \Longrightarrow \text{Map} ( f \circ g )\)】/\({\circ}.\)◀ O
上の定理OK。下はなぜか×
定義域の制限
word(cc,c)! …【\({\sf R} | _{ {\sf C} }\)】def …【\({\sf R} | _{ {\sf C} }\)】≃【\(\{ \langle {\sf x} , {\sf y} \rangle \in {\sf R} \mid {\sf x} \in {\sf C} \}\)】
word(ss,s)! …【\({\sf R} | _{ {\sf X} }\)】
\(|.\)【\({\sf R} | _{ {\sf X} } = {\sf R} | _{ {\sf X} }\)】
\(|\text{id}\)【\(\text{Rel} ( R ) \Longrightarrow R | _{ X } = R \circ \text{id} | _{ X }\)】
集合上の写像
word(s,c) … \(\text{mapon} \)def …【\(\text{mapon} ( {\sf X} )\)】≃【\(\{ {\sf f} \mid \text{Map} ( {\sf f} ) , \text{dom} ( {\sf f} ) = {\sf X} \} \)】
\(\text{mapon0}\)【\(\text{mapon} ( \emptyset ) = \{ \emptyset \}\)】
word(ss,s) … \(\to\)
\({\to}.\)【\(X \to Y = \{ f \in \text{mapon} ( X ) \mid \text{rng} ( f ) \subset Y \}\)】
写像への代入
写像への代入に当たるものを作ります。word(ss,s)! …【\({\sf F} ( {\sf X} )\)】
\(\text{ap0}\)【\(x \in \text{dom} ( f ) \Rightarrow \langle x , f ( x ) \rangle \in f\)】
このThmは選択公理を導いてしまいます。
word(ss,s) … \(\mapsto\)
def …【\({\sf x} \mapsto {\sf y}\)】≃【\(\{ \langle {\sf x} , {\sf y} \rangle \}\)】
\({\mapsto}0\)【\(( x \mapsto y ) ( x ) = y\)】◀ \(\text{set}_1.\)\(\text{ap0}\)/\(\text{dom.}\)
\(\text{sep_map}\)【\(f \in \text{mapon} ( X ) \Longrightarrow f = \bigcup _{ x \in X } ( x \mapsto f ( x ) )\)】