写像
word(,c) … \(\text{Map}\)def …【\(\text{Map}\)】≃【\(\{ f \in \text{Rel} \mid \forall x \, ! y \, \langle x , y \rangle \in f \}\)】
abbr …【\(\langle {\sf f} \rangle\)】≈【\(\{ \langle {\sf x} , {\sf f} {\sf x} \rangle \mid {\sf x} \in \text{Set} \}\)】
word(s,s)と写像は等価です。\({\sf f} {\sf X} = {\sf Y} \Longleftrightarrow \langle {\sf X} , {\sf Y} \rangle \in \langle {\sf f} \rangle\)
word(s,c)F … \(\text{mapon} \)
def …【\(\text{mapon} ( {\sf X} )\)】≃【\(\{ {\sf f} \in \text{Map} \mid \text{dom} ( {\sf f} ) = {\sf X} \}\)】
\(\text{mapon0}\)【\(\text{mapon} ( \emptyset ) = \{ \emptyset \}\)】\({\bf /}\text{set}_1.{\bf /}\emptyset{.}{.}{\bf /}\text{dom.}\) ◀ O
word(ss,s) … \(\to\)
\({\to}.\)【\(X \to Y = \{ f \in \text{mapon} ( X ) \mid \text{rng} ( f ) \subset Y \}\)】
\(\text{Map0}\)【\(f \in \text{Map} \Longrightarrow f \in \text{dom} ( f ) \to \text{rng} ( f )\)】\({\bf /}{\to}.\) ◀ \({\subset}自\)
\({\circ}\text{Map}\)【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in \text{Map}\)】\({\bf /}{\to}.{\bf /}{\circ}.\) ◀ \(\text{%0}\)
\({\circ}\text{Map2}\)【\(f \in X \to Y , g \in Y \to Z \Longrightarrow \text{rng} ( g \circ f ) \subset Z\)】\({\bf /}{\to}.\) ◀ \(\text{%0}\,{\bf ,}\,\text{dom.}\,{\bf ,}\,\text{rng.}\,{\bf ,}\,{\subset.}\,{\bf ,}\,{\circ}.\)
ここまでOK
\({\circ}\text{Map1}\)【\(f \in X \to Y , g \in Y \to Z \Longrightarrow \text{dom} ( g \circ f ) = X\)】\({\bf /}{\to}.\) ◀ \(\text{%0}\,{\bf ,}\,\text{dom.}\,{\bf ,}\,\text{rng.}\,{\bf ,}\,{=.}\,{\bf ,}\,{\circ}.\)
分割すれば示せる
写像の例
word(cc,c)! …【\({\sf Y} _{ \mid {\sf X} }\)】def …【\({\sf Y} _{ \mid {\sf X} }\)】≃【\({\sf X} \times \{ {\sf Y} \}\)】
\(\text{on0}\)【\(X \to \{ y \} = \{ y _{ \mid X } \}\)】\(\) ◀ \({=.}\text{set}_1.\)
写像を作るときには\(\lambda\)計算の書式が便利です。
abbr …【\([ {\sf x} {\sf A} \mid {\sf X} ]\)】≈【\(\{ \langle {\sf x} , {\sf X} \rangle \mid {\sf x} {\sf A} \}\)】
word(s,s)! …【\(\text{id} _{ {\sf X} }\)】
\(\text{id}.\)【\(\text{id} _{ X } = [ x \in X \mid x ]\)】
定義域の制限
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(ss,s)! …【\({\sf F} ( {\sf X} )\)】\(\text{ap0}\)【\(f \in \text{mapon} ( X ) , x \in X \Longrightarrow \langle x , f ( x ) \rangle \in f\)】
\(\text{Map1}\)【\(f \in \text{mapon} ( X ) \Longrightarrow f = [ x \in X \mid f ( x ) ]\)】