2 写像

2.1 写像の集合

word(sc,c) … \(\to\)
→_. … \(X \to Y = \{ f \subset X \times Y \mid X \subset {\hat\triangleleft!} ( f ) \}\)
word(ss,s) … \(\to\)
→. … \([\to] \stackrel{\star\!\star}{=} [\to]\)
\(f \in X \to \mathbb{V} \Longleftrightarrow f \in X \to {\hat\triangleright} ( f ) \Longleftrightarrow \exists Y f \in X \to Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→.. … \(X \to Y = \{ f \in X \to \mathbb{V} \mid {\hat\triangleright} ( f ) \subset Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\emptyset \to X = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→∘ … \(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.2 制限

word(ss,s) … \(|\)
rest. … \(R | _ X = \{ \langle x , y \rangle \in R \mid x \in X \}\)
→rest … \(f \in X \to Y \Longrightarrow f | _ A \in X \cap A \to Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word((s,s)s,s) … \(|\)
Rest. … \(F | _ X = \{ p \mid \exists x \in X . p = \langle x , F ( x ) \rangle \}\)
→_.𝕍 … \(f \in X \to \mathbb{V} \Longleftrightarrow f = \lceil f ( \bullet ) \rfloor | _ X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(f , g \in X \to \mathbb{V} \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.3 一点集合と写像

\(\{ x \} \to Y = \{ \{ \langle x , y \rangle \} \mid y \in Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \times Y = \bigcup _{ x \in X , y \in Y } \{ \langle x , y \rangle \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

word(ss,s) … \(|\)
on. … \(y | _ X = \lceil x \mapsto y \rfloor | _ X\)
\(y | _ X = X \times \{ y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \to \{ y \} = \{ y | _ X \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.4 写像の和

→cup … \(\begin{cases} f_{1} \in X_{1} \to \mathbb{V} \\ f_{2} \in X_{2} \to \mathbb{V} \end{cases} , \forall x \in X_{1} \cap X_{2} . f_{1} ( x ) = f_{2} ( x ) \Longrightarrow \begin{cases} f_{1} \cup f_{2} \in X_{1} \cup X_{2} \to \mathbb{V} \\ \forall x \in X_{1} . ( f_{1} \cup f_{2} ) ( x ) = f_{1} ( x ) \\ \forall x \in X_{2} . ( f_{1} \cup f_{2} ) ( x ) = f_{2} ( x ) \end{cases}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
→cup2 … \(\begin{cases} f_{1} \in X_{1} \to Y_{1} \\ f_{2} \in X_{2} \to Y_{2} \end{cases} , \forall x \in X_{1} \cap X_{2} . f_{1} ( x ) = f_{2} ( x ) \Longrightarrow f_{1} \cup f_{2} \in ( X_{1} \cup X_{2} ) \to ( Y_{1} \cup Y_{2} )\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.5 Knaster-Tarskiの不動点定理

KT … \(f \in \wp X \to \wp X , \forall A , B \, A \subset B \subset X \Longrightarrow f ( A ) \subset f ( B ) \Longrightarrow \exists A \in \wp X . f ( A ) = A\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s