順序対およびその使用についての基本諸事項を整備します。\(\dagger\)
最初の使用例として、置換公理の簡潔な記述を与えます。その後に分出公理も与えます。\(\dagger\)
順序対の集合は関係と呼ばれ、写像が特別な関係として定義されます。\(\dagger\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
word(s,s) … \(\triangleleft\) \(\triangleright\)
pr<. … \(\triangleleft \langle x , y \rangle = x\)
pr>. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) W.
*^ap_. … \(R ( X ) = \{ y \mid \exists x \in X . \langle x , y \rangle \in R \}\)
word(c,c)F … \({!_\triangleleft}\)
pr<!. … \({!_\triangleleft} ( R ) = \{ x \mid \, ! y \, \langle x , y \rangle \in R \}\)
word(c,p) … \(\text{ax_r}\)
ax_r. … \(\text{ax_r} ( R ) \Longleftrightarrow \forall X \subset {!_\triangleleft} ( R ) . \dot\exists R ( X )\)
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.
Le_set2 … \(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) wp. / sub. ，\0.
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) Ax_r ，Le_set2 ，pr:0
cvt … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
\(\dot\exists \stackrel{\text{^}}{\mathop{{\sf f}}} A\) というのが置換公理です(？)
word(ss,s→ss,c) … \(\text{^*}\) \(\text{*^}\) \(\text{^^}\)
cvt … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
cvt … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
cvt … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)
ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \exists X \, C \subset X \Rightarrow \dot\exists C\)
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) Ax_s
\(C \subset X \Rightarrow \dot\exists C\) \(\blacktriangleleft\) Ax_r ，pr:0
^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 \}\)
word(s,s)F … \(\triangleleft\) \(\triangleright\)
^pr<. … \({\triangleleft} \stackrel{\star}{=} {\triangleleft}\)
^pr>. … \({\triangleright} \stackrel{\star}{=} {\triangleright}\)
^^pr_. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
word(ss,s) … \(\times\)
^^pr. … \({\times} \stackrel{\star\!\star}{=} {\times}\)
\({\times} \stackrel{\star\!\star}{=} \; \stackrel{\text{^^}}{\mathsf{pr}}\) \(\blacktriangleleft\) W.
word(,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\) W.
Rel.. … \(\text{Rel} = \{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\) \(\blacktriangleleft\) W.
\(R \in \text{Rel} \Longrightarrow \triangleleft ( R ) = \stackrel{\text{^}}{\triangleleft} ( R ) , \triangleright ( R ) = \stackrel{\text{^}}{\triangleright} ( R )\) \(\blacktriangleleft\) W.
^pr<!. … \(\triangleleft! ( R ) = \triangleleft ( R ) \cap {!_\triangleleft} ( R )\)
word(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\) W.
word(ss,s) … *^ap
*^ap. … [*^ap] {**}=_ [*^ap_]
*^ap:0 … \(A \subset \triangleleft! ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\) \(\blacktriangleleft\) W.
sw:I … \(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\) \(\blacktriangleleft\) W.
word(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\) W.
^sw:I … \(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\) \(\blacktriangleleft\) W.
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\) W.
comp:A … \(R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\) \(\blacktriangleleft\) W.
comp:X … \(R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\) \(\blacktriangleleft\) W.
comp_ap … \(x \in \triangleleft! ( f ) , f ( x ) \in \triangleleft! ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\) \(\blacktriangleleft\) W.
\(( \wp ( X \times X ) , {\circ} ) :\underline{2}\&\mathsf{A}\) \(\blacktriangleleft\)
->_. … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\)
word(ss,s) … \(\to\)
->. … \({\to} \stackrel{\star\!\star}{=} {\to}\)
->.' … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\) \(\blacktriangleleft\) W.
\(f \in X \to \mathbb{V} \Longleftrightarrow f \in X \to \triangleright ( f ) \Longleftrightarrow \exists Y f \in X \to Y\) \(\blacktriangleleft\) W.
->.. … \(X \to Y = \{ f \in X \to \mathbb{V} \mid \forall x \in X . f ( x ) \in Y \}\) \(\blacktriangleleft\) W.
->..' … \(X \to Y = \{ f \in X \to \mathbb{V} \mid \triangleright ( f ) \subset Y \}\) \(\blacktriangleleft\) W.
\(\emptyset \to X = \{ \emptyset \}\) \(\blacktriangleleft\) W.
\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\) \(\blacktriangleleft\) W.
->comp … \(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\) \(\blacktriangleleft\) W.
word(,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\) W.
abbr … \(\{ x \mapsto X \}\) ≈ \(\mathsf{fn} x ( X )\)
cvt … \(\{ x \mapsto X \} ( T )\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例 \(\{ \bullet + a \}\) ≈ \(\{ x \mapsto x + a \}\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 \(\{ \bullet + \{ \bullet + a \} ( x ) \}\) ≃ \(\{ \bullet + ( x + a ) \}\)
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\) W.
word((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\) W.
\(f , g \in X \to \mathbb{V} \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\) \(\blacktriangleleft\) W.
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\) W.
\(\{ x \} \to Y = \{ x \mathop{{\cdot}{\to}} y \mid y \in Y \}\) \(\blacktriangleleft\) W.
\(X \times Y = \bigcup _{ x \in X , y \in Y } ( x \mathop{{\cdot}{\to}} y )\) \(\blacktriangleleft\) W.
word(ss,s) … \(|\)
on. … \(y | _ X = \{ x \mapsto y \} | X\)
\(y | _ X = X \times \{ y \}\) \(\blacktriangleleft\) W.
\(X \to \{ y \} = \{ y | _ X \}\) \(\blacktriangleleft\) W.
->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\) W. ，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\) W. ，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\) W. ，pr:0
->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\) W.
->I.'' … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \triangleright ( f ) \to X \}\) \(\blacktriangleleft\) W.
->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\) W.
->S.'' … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \triangleright ( f ) = Y \}\) \(\blacktriangleleft\) W.
->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\) W.
->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\) W.
->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\) W.
->IS_^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^\leftrightarrow \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) W.
->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\) W.
->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\) W.
->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\) W.
id. … \(\text{id} _ X = \{ \bullet \} | X\)
id:0 … \(\text{id} _ X \in X \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) W.
comp:E … \(R \subset X \times Y \Longrightarrow R \circ \text{id} _ X = R = \text{id} _ Y \circ R\) \(\blacktriangleleft\) W.
\(R \in \text{Rel} \Longrightarrow R | _ X = R \circ \text{id} _ X\) \(\blacktriangleleft\) W.
->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\) W.
\(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\) W.
\(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\) W. ，Ax_s
最初の使用例として、置換公理の簡潔な記述を与えます。その後に分出公理も与えます。\(\dagger\)
順序対の集合は関係と呼ばれ、写像が特別な関係として定義されます。\(\dagger\)
b1
順序対
word(ss,s)F … \(\mathsf{pr}\)abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
word(s,s) … \(\triangleleft\) \(\triangleright\)
pr<. … \(\triangleleft \langle x , y \rangle = x\)
pr>. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) W.
置換公理
word(cc,c) … *^ap_*^ap_. … \(R ( X ) = \{ y \mid \exists x \in X . \langle x , y \rangle \in R \}\)
word(c,c)F … \({!_\triangleleft}\)
pr<!. … \({!_\triangleleft} ( R ) = \{ x \mid \, ! y \, \langle x , y \rangle \in R \}\)
word(c,p) … \(\text{ax_r}\)
ax_r. … \(\text{ax_r} ( R ) \Longleftrightarrow \forall X \subset {!_\triangleleft} ( R ) . \dot\exists R ( X )\)
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.
Le_set2 … \(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) wp. / sub. ，\0.
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) Ax_r ，Le_set2 ，pr:0
関数の像
word(s,s→s,c) … \(\text{^}\)cvt … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
\(\dot\exists \stackrel{\text{^}}{\mathop{{\sf f}}} A\) というのが置換公理です(？)
word(ss,s→ss,c) … \(\text{^*}\) \(\text{*^}\) \(\text{^^}\)
cvt … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
cvt … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
cvt … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)
分出公理
word(c,p) … \(\text{ax_s}\)ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \exists X \, C \subset X \Rightarrow \dot\exists C\)
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) Ax_s
\(C \subset X \Rightarrow \dot\exists C\) \(\blacktriangleleft\) Ax_r ，pr:0
b2
定義域・値域
word(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 \}\)
word(s,s)F … \(\triangleleft\) \(\triangleright\)
^pr<. … \({\triangleleft} \stackrel{\star}{=} {\triangleleft}\)
^pr>. … \({\triangleright} \stackrel{\star}{=} {\triangleright}\)
直積、関係
word(cc,c) … \(\times\)^^pr_. … \(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\)
word(ss,s) … \(\times\)
^^pr. … \({\times} \stackrel{\star\!\star}{=} {\times}\)
\({\times} \stackrel{\star\!\star}{=} \; \stackrel{\text{^^}}{\mathsf{pr}}\) \(\blacktriangleleft\) W.
word(,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\) W.
Rel.. … \(\text{Rel} = \{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\) \(\blacktriangleleft\) W.
\(R \in \text{Rel} \Longrightarrow \triangleleft ( R ) = \stackrel{\text{^}}{\triangleleft} ( R ) , \triangleright ( R ) = \stackrel{\text{^}}{\triangleright} ( R )\) \(\blacktriangleleft\) W.
(s,s)の方が自然？
代入
word(c,c)F … \(\triangleleft!\)^pr<!. … \(\triangleleft! ( R ) = \triangleleft ( R ) \cap {!_\triangleleft} ( R )\)
word(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\) W.
word(ss,s) … *^ap
*^ap. … [*^ap] {**}=_ [*^ap_]
*^ap:0 … \(A \subset \triangleleft! ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\) \(\blacktriangleleft\) W.
成分の入れ替え
sw. … \(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)sw:I … \(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\) \(\blacktriangleleft\) W.
word(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\) W.
^sw:I … \(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\) \(\blacktriangleleft\) W.
合成
word(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\) W.
comp:A … \(R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\) \(\blacktriangleleft\) W.
comp:X … \(R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\) \(\blacktriangleleft\) W.
comp_ap … \(x \in \triangleleft! ( f ) , f ( x ) \in \triangleleft! ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\) \(\blacktriangleleft\) W.
\(( \wp ( X \times X ) , {\circ} ) :\underline{2}\&\mathsf{A}\) \(\blacktriangleleft\)
b3
cc,cではなくsc,cにすべき
写像
word(cc,c) … \(\to\)->_. … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\)
word(ss,s) … \(\to\)
->. … \({\to} \stackrel{\star\!\star}{=} {\to}\)
->.' … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\) \(\blacktriangleleft\) W.
\(f \in X \to \mathbb{V} \Longleftrightarrow f \in X \to \triangleright ( f ) \Longleftrightarrow \exists Y f \in X \to Y\) \(\blacktriangleleft\) W.
->.. … \(X \to Y = \{ f \in X \to \mathbb{V} \mid \forall x \in X . f ( x ) \in Y \}\) \(\blacktriangleleft\) W.
->..' … \(X \to Y = \{ f \in X \to \mathbb{V} \mid \triangleright ( f ) \subset Y \}\) \(\blacktriangleleft\) W.
\(\emptyset \to X = \{ \emptyset \}\) \(\blacktriangleleft\) W.
\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\) \(\blacktriangleleft\) W.
->comp … \(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\) \(\blacktriangleleft\) W.
word(,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\) W.
アロー関数
word(vs,(s,s)) … \(\mathsf{fn}\)abbr … \(\{ x \mapsto X \}\) ≈ \(\mathsf{fn} x ( X )\)
cvt … \(\{ x \mapsto X \} ( T )\) ≃ \(T\) の \(x\) に \(X\) を代入したもの
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。
例 \(\{ \bullet + a \}\) ≈ \(\{ x \mapsto x + a \}\)
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 \(\{ \bullet + \{ \bullet + a \} ( x ) \}\) ≃ \(\{ \bullet + ( x + a ) \}\)
定義域の制限
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\) W.
word((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\) W.
\(f , g \in X \to \mathbb{V} \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\) \(\blacktriangleleft\) W.
一点集合と写像
word(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\) W.
\(\{ x \} \to Y = \{ x \mathop{{\cdot}{\to}} y \mid y \in Y \}\) \(\blacktriangleleft\) W.
\(X \times Y = \bigcup _{ x \in X , y \in Y } ( x \mathop{{\cdot}{\to}} y )\) \(\blacktriangleleft\) W.
word(ss,s) … \(|\)
on. … \(y | _ X = \{ x \mapsto y \} | X\)
\(y | _ X = X \times \{ y \}\) \(\blacktriangleleft\) W.
\(X \to \{ y \} = \{ y | _ X \}\) \(\blacktriangleleft\) W.
写像の和
場合分けをして写像を作ることがあります。まず貼り合わせた写像の値を計算します。->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\) W. ，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\) W. ，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\) W. ，pr:0
未完
b4
単射、全射①
word(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\) W.
->I.'' … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \triangleright ( f ) \to X \}\) \(\blacktriangleleft\) W.
->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\) W.
->S.'' … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \triangleright ( f ) = Y \}\) \(\blacktriangleleft\) W.
->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\) W.
->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\) W.
->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\) W.
単射、全射②
->S:0 … \(f \in X \to \mathbb{V} \Longrightarrow f \in X \stackrel{\rm S}\to \triangleright ( f )\) \(\blacktriangleleft\) W.->IS_^sw … \(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^\leftrightarrow \in Y \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) W.
->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\) W.
->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\) W.
->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\) W.
恒等写像
word(s,s) … \(\text{id}\)id. … \(\text{id} _ X = \{ \bullet \} | X\)
id:0 … \(\text{id} _ X \in X \stackrel{\rm IS}\to X\) \(\blacktriangleleft\) W.
comp:E … \(R \subset X \times Y \Longrightarrow R \circ \text{id} _ X = R = \text{id} _ Y \circ R\) \(\blacktriangleleft\) W.
\(R \in \text{Rel} \Longrightarrow R | _ X = R \circ \text{id} _ X\) \(\blacktriangleleft\) W.
->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\) W.
\(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\) W.
\(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\) W. ，Ax_s
右逆射が存在することは選択公理と同値