a
定義域・値域
\(\mathbb{W}_1\)(c,c)F … \(\triangleleft\) \(\triangleright\)^pr<_. … \(\triangleleft ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)
^pr>_. … \(\triangleright ( R ) = \{ y \mid \exists x \, \langle x , y \rangle \in R \}\)
\(\mathbb{W}_0\)(s,s)F … \(\triangleleft\) \(\triangleright\)
^pr<. … \({\triangleleft} \stackrel{\star}{=} {\triangleleft}\)
^pr>. … \({\triangleright} \stackrel{\star}{=} {\triangleright}\)
直積、関係
\(\mathbb{W}_1\)(cc,c) … \(\times\)^^pr_. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
\(\mathbb{W}_0\)(ss,s) … \(\times\)
^^pr. … \({\times} \stackrel{\star\!\star}{=} {\times}\)
\({\times} \stackrel{\star\!\star}{=} \; {\stackrel{\text{^^}}{\mathsf{pr}}}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_1\)(,c) … \(\text{Rel}\)
Rel. … \(\text{Rel} = \{ R \mid R \subset \mathbb{V} \times \mathbb{V} \}\)
Rel.' … \(\text{Rel} = \{ R \mid R \subset \triangleleft ( R ) \times \triangleright ( R ) \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Rel.. … \(\text{Rel} = \{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(R \in \text{Rel} \Longrightarrow \triangleleft ( R ) = \stackrel{\text{^}}{\triangleleft} ( R ) , \triangleright ( R ) = \stackrel{\text{^}}{\triangleright} ( R )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
(s,s)の方が自然？
代入
\(\mathbb{W}_1\)(c,c)F … \(\triangleleft!\)^pr<!. … \(\triangleleft! ( R ) = \triangleleft ( R ) \cap {!_\triangleleft} ( R )\)
\(\mathbb{W}_0\)(fs,s) … ap
ap. … \(x \in \triangleleft! ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)
ap:0 … \(x \in \triangleleft! ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(ss,s) … *^ap
*^ap. … [*^ap] {**}=_ [*^ap_]
*^ap:0 … \(A \subset \triangleleft! ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
成分の入れ替え
sw. … \(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)sw:I … \(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(s,s) … \(^\leftrightarrow\)
^sw. … \({^\leftrightarrow} \stackrel{\star}{=} \; {\stackrel{\text{^}}{^\leftrightarrow}}\)
^sw:0 … \(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
^sw:I … \(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
合成
\(\mathbb{W}_0\)(ss,s) … \(\circ\)comp. … \(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)
comp:0 … \(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
comp:A … \(R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
comp:X … \(R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
comp_ap … \(x \in \triangleleft! ( f ) , f ( x ) \in \triangleleft! ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( \wp ( X \times X ) , {\circ} ) :\underline{2}\&\mathsf{A}\) \(\blacktriangleleft\)
b
写像
\(\mathbb{W}_1\)(sc,c) … \(\to\)->_. … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\)
\(\mathbb{W}_0\)(ss,s) … \(\to\)
->. … \({\to} \stackrel{\star\!\star}{=} {\to}\)
->.' … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(f \in X \to \mathbb{V} \Longleftrightarrow f \in X \to \triangleright ( f ) \Longleftrightarrow \exists Y f \in X \to Y\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->.. … \(X \to Y = \{ f \in X \to \mathbb{V} \mid \forall x \in X . f ( x ) \in Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->..' … \(X \to Y = \{ f \in X \to \mathbb{V} \mid \triangleright ( f ) \subset Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \to X = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->comp … \(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_1\)(,c) … \(\text{Map}\)
Map. … \(\text{Map} = \{ f \mid f \in \triangleleft ( f ) \to \mathbb{V} \}\)
Map.. … \(\text{Map} = \{ f \in \text{Rel} \mid \triangleleft ( f ) \subset {!_\triangleleft} ( f ) \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
定義域の制限
\(\mathbb{W}_0\)(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}_0.\)
\(\mathbb{W}_1\)((s,s)s,s) … \(|\)
Rest. … \(F | X = \{ p \mid \exists x \in X . p = \langle x , F ( x ) \rangle \}\)
->_.V … \(f \in X \to \mathbb{V} \Longleftrightarrow f = [ f ( \bullet ) ] | X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(f , g \in X \to \mathbb{V} \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
一点集合と写像
\(\mathbb{W}_0\)(ss,s) … \(\mathop{{\cdot}{\to}}\)mto. … \(p \in x \mathop{{\cdot}{\to}} y \Longleftrightarrow p = \langle x , y \rangle\)
mto.' … \(x \mathop{{\cdot}{\to}} y = \{ \langle x , y \rangle \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\{ x \} \to Y = \{ x \mathop{{\cdot}{\to}} y \mid y \in Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \times Y = \bigcup _{ x \in X , y \in Y } ( x \mathop{{\cdot}{\to}} y )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(ss,s) … \(|\)
on. … \(y | _ X = [ x \mapsto y ] | X\)
\(y | _ X = X \times \{ y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \to \{ y \} = \{ y | _ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
写像の和
場合分けをして写像を作ることがあります。まず貼り合わせた写像の値を計算します。->cup1 … \(\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} \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}_0.\) ，pr:0
貼り合わせた写像は写像になります。
->cup0 … \(f_{1} \in X_{1} \to \mathbb{V} , f_{2} \in X_{2} \to \mathbb{V} , \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 \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，pr:0
値域つきの貼り合わせ（証明は ->_ 非展開仕様の実装後）。
->cup2 … \(f_{1} \in X_{1} \to Y_{1} , f_{2} \in X_{2} \to Y_{2} , \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}\)
以下は須田作->cup0 … \(f_{1} \in X_{1} \to \mathbb{V} , f_{2} \in X_{2} \to \mathbb{V} , \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 \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，pr:0
未完
c
単射、全射①
\(\mathbb{W}_0\)(ss,s) … \(\stackrel{\rm I}\to\) \(\stackrel{\rm S}\to\) \(\stackrel{\rm IS}\to\)->I. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\)
->I.' … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \triangleright ( f ) \to \mathbb{V} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->I.'' … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \triangleright ( f ) \to X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->S. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \, \langle x , y \rangle \in f \}\)
->S.' … \(X \stackrel{\rm S}\to Y = \{ f \in X \to \mathbb{V} \mid \triangleright ( f ) = Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->S.'' … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \triangleright ( f ) = Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->IS. … \(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)
->IS.. … \(X \stackrel{\rm IS}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in Y \to X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->I.. … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall^* x_{0} , x_{1} \in X . f ( x_{0} ) \neq f ( x_{1} ) \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->S.. … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \in X . y = f ( x ) \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
単射、全射②
->S:0 … \(f \in X \to \mathbb{V} \Longrightarrow f \in X \stackrel{\rm S}\to \triangleright ( f )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)->IS_^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^\leftrightarrow \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->I_comp … \(f \in X \stackrel{\rm I}\to Y , g \in Y \stackrel{\rm I}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm I}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->S_comp … \(f \in X \stackrel{\rm S}\to Y , g \in Y \stackrel{\rm S}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm S}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->IS_comp … \(f \in X \stackrel{\rm IS}\to Y , g \in Y \stackrel{\rm IS}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm IS}\to Z\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
恒等写像
\(\mathbb{W}_0\)(s,s) … \(\text{id}\)id. … \(\text{id} _ X = [ \bullet ] | X\)
id:0 … \(\text{id} _ X \in X \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
comp:E … \(R \subset X \times Y \Longrightarrow R \circ \text{id} _ X = R = \text{id} _ Y \circ R\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(R \in \text{Rel} \Longrightarrow R | _ X = R \circ \text{id} _ X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
->I.i … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \circ f = \text{id} _ X \} = \{ f \in X \to Y \mid \exists g \, g \circ f = \text{id} _ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid f \circ f ^\leftrightarrow = \text{id} _ Y \} = \{ f \in X \to Y \mid \exists g \, f \circ g = \text{id} _ Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \neq \emptyset \Longrightarrow X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \exists g \in Y \to X . g \circ f = \text{id} _ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，Ax_s
右逆射が存在することは選択公理と同値