1 - b　順序対、写像 - atp-research.com

b1

順序対も基本的です。\(\dagger\)

最初の使用例として置換公理の簡潔な記述を取り上げます。

順序対

word(ss,s)F … \(\text{pr}\)
abbr …【\(\langle x , y \rangle\)】≈【\(\text{pr} ( x , y )\)】

次のものは対の成分を取り出します。
word(s,s) … \(\triangleleft\) \(\triangleright\)
pr<.【\(\triangleleft \langle x , y \rangle = x\)】
pr>.【\(\triangleright \langle x , y \rangle = y\)】
pr0【\(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\)】\(\blacktriangleleft\)

置換公理

像を作る記号は表記を持たず\(R ( X )\)という形で使用されます。
word(cc,c) … ap__
ap__.【\(R ( X ) = \{ y \mid \exists x \in X . \langle x , y \rangle \in R \}\)】

像は適切な条件の下で集合になります。
word(c,p) … \(\text{ax_r}\)
ax_r.【\(\text{ax_r} ( R ) \Longleftrightarrow \forall X ( \forall x \in X . ! y \, \langle x , y \rangle \in R \Rightarrow \dot\exists ( R ( X ) ) )\)】
c-Form \({\tt R}\) に対して `ax_r(\({\tt R}\))` が公理に含まれます。

対集合公理は他の公理から導出されます。未完！
【\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\)】\(\blacktriangleleft\)
分出公理は置換公理から導出されます。未完！

関数の像

word関数 … 表記の無い #p : (s,s)→(s,c)
cvt …【\({\mathop{{\sf f}}} \, A\)】≃【\(\{ \mathop{{\sf f}} a \mid a \in A \}\)】
【\(\dot\exists \, {\mathop{{\sf f}}} \, A\)】というのが置換公理です(？)
word関数 … 表記の無い #l , #r , #P : (ss,s)→(ss,c)
cvt …【\(A \, {\mathop{{\sf f}}} \, b\)】≃【\(\{ a \mathop{{\sf f}} b \mid a \in A \}\)】
cvt …【\(a \, {\mathop{{\sf f}}} \, B\)】≃【\(\{ a \mathop{{\sf f}} b \mid b \in B \}\)】
cvt …【\(A \, {\mathop{{\sf f}}} \, B\)】≃【\(\{ a \mathop{{\sf f}} b \mid a \in A , b \in B \}\)】

#pを#^, #lを#^-,#rを#-^,#Pを#^^に

b2

対や対の集合に関わる諸操作を準備します。

関係

対の集合は関係と呼ばれます。
word(,c) … \(\text{Rel}\)
Rel.【\(\text{Rel} = \{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\)】

直積、定義域・値域を作ります。
word(ss,s) … \(\times\)
pr^^. {pr^^ **=_ #Ppr}
word(s,s)F … \(\text{dom}\) \(\text{im}\)
dom.【\(\text{dom} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)】
im.【\(\text{im} ( R ) = \{ y \mid \exists x \, \langle x , y \rangle \in R \}\)】
【\(R \in \text{Rel} \Rightarrow \text{dom} ( R ) = {\triangleleft} R\)】\(\blacktriangleleft\)
【\(\text{Rel} = \{ R \mid R \subset \text{dom} ( R ) \times \text{im} ( R ) \}\)】\(\blacktriangleleft\)

定義域の制限
word(ss,s) … \(|\)
rest.【\(R | _ X = \{ \langle x , y \rangle \in R \mid x \in X \}\)】

\(\triangleleft(R),\triangleright(R)\) でいいじゃね？

b3

当システムでは写像は特別な関係として定義されます。\(\dagger\)

写像であることを示す時、写像であることを利用する時、諸状況によって定義の使い分けが有効です。

写像①

word(,c) … \(\text{Ndeg}\)
Ndeg.【\(\text{Ndeg} = \{ f \mid \forall x \, ! y \, \langle x , y \rangle \in f \}\)】
Ndeg..【\(\text{Ndeg} = \{ f \mid \forall x \forall y \, ( \langle x , y \rangle \in f \Rightarrow y = f ( x ) ) \}\)】\(\blacktriangleleft\)
`f in_ Ndeg` {Ndeg..} 想定外になる

word(s,c) … \(\text{mapon} \)
mapon.'【\(\text{mapon} ( X ) = \{ f \in \text{Rel} \cap \text{Ndeg} \mid \text{dom} ( f ) = X \}\)】
【\( f , g \in \text{mapon} ( X ) \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\)】\(\blacktriangleleft\)

一項関数の制限により写像が作られます。ただしクラスであることに注意。
abbr …【\( \mathop{{\sf f}} _ X\)】≈【\(\{ \langle x , \mathop{{\sf f}} x \rangle \mid x \in X \}\)】
【\(\text{mapon} ( X ) = \{ f \mid f = [ f ( \bullet ) ] _ X \}\)】\(\blacktriangleleft\)

写像②

word(ss,s) … \(\to\)
->.【\(X \to Y = \{ f \subset X \times Y \mid X \subset \text{dom!} ( f ) \}\)】
->..'【\(X \to Y = \{ f \in \text{mapon} ( X ) \mid \text{im} ( f ) \subset Y \}\)】\(\blacktriangleleft\)
【\(\emptyset \to X = \{ \emptyset \}\)】\(\blacktriangleleft\)
【\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\)】\(\blacktriangleleft\)
->comp【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\)】\(\blacktriangleleft\)
->rest【\(f \in X \to Y \Longrightarrow f | _ A \in X \cap A \to Y\)】\(\blacktriangleleft\)

写像の特徴づけ。未完
【\(\text{Rel} \cap \text{Ndeg} = \{ f \mid f \in \text{dom} ( f ) \to \text{im} ( f ) \} = \{ f \mid \exists X \exists Y f \in X \to Y \}\)】\(\blacktriangleleft\)

一点集合と写像

word(ss,s) … \(\mathop{{\cdot}{\to}}\)
mto.'【\(x \mathop{{\cdot}{\to}} y = \{ \langle x , y \rangle \}\)】
【\(\{ x \} \to Y = \{ x \mathop{{\cdot}{\to}} y \mid y \in Y \}\)】\(\blacktriangleleft\)
【\(X \times Y = \bigcup _{ x \in X , y \in Y } ( x \mathop{{\cdot}{\to}} y )\)】\(\blacktriangleleft\)

word(ss,s) … \(|\)
on.【\(y | _ X = [ x \mapsto y ] _ X\)】
【\(y | _ X = X \times \{ y \}\)】\(\blacktriangleleft\)
【\(X \to \{ y \} = \{ y | _ X \}\)】\(\blacktriangleleft\)

単射、全射

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 f ^\leftrightarrow \in \text{im} ( f ) \to X \}\)】
->S.'【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{im} ( f ) = Y \}\)】
->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\)

->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\)
->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\)

恒等写像

word(s,s) … \(\text{id}\)
id.【\(\text{id} _ X = [ \bullet ] _ X\)】
id0【\(\text{id} _ X \in X \stackrel{\rm IS}\to X\)】\(\blacktriangleleft\)
comp単【\(R \subset X \times Y \Longrightarrow R \circ \text{id} _ X = R = \text{id} _ Y \circ R\)】\(\blacktriangleleft\)
【\(R \in \text{Rel} \Longrightarrow R | _ X = R \circ \text{id} _ X\)】\(\blacktriangleleft\)

【\(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\)
【\(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\)

写像の和

場合分けをして写像を作ることがあります。
【\(f_{1} \in \text{mapon} ( X_{1} ) , f_{2} \in \text{mapon} ( X_{2} ) , X_{1} \cap X_{2} = \emptyset \Longrightarrow f_{1} \cup f_{2} \in \text{mapon} ( X_{1} \cup X_{2} )\)】\(\blacktriangleleft\)

未完

b4

基数とかめんどくさいので濃度の定義もしません。「２つの集合の濃度が等しいか？」という事は議論します。

濃度

word(ss,p) … \(\stackrel{\#}=\) \(\stackrel{\#}\le\) \(\stackrel{\#}<\)
=#.'【\(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)】
le#.'【\(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\)】
<#.【\(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \cancel{\stackrel{\#}=} Y\)】

=#0【\(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\)】\(\blacktriangleleft\)

濃度

->ISsw_【\(f \in X \stackrel{\rm IS}\to Y \Longrightarrow f ^\leftrightarrow \in Y \stackrel{\rm IS}\to X\)】\(\blacktriangleleft\)

->Icomp【\(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\)
->Scomp【\(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\)
->IScomp【\(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\)

=#ITX【\(\stackrel{\#}= {:}\, \text{I} \text{T} \text{X}\)】\(\blacktriangleleft\)
le#IT【\(\stackrel{\#}\le {:}\, \text{I} \text{T}\)】\(\blacktriangleleft\)
sub_le#【\(X \subset Y \Rightarrow X \stackrel{\#}\le Y\)】\(\blacktriangleleft\)

濃度の制限

【\(X \times Y \stackrel{\#}= Y \times X\)】\(\blacktriangleleft\)
【\(X \to ( Y \to Z ) \stackrel{\#}= X \times Y \to Z\)】\(\blacktriangleleft\)

Cantorの定理
<#wp【\(X \stackrel{\#}< \wp X\)】\(\blacktriangleleft\)
準備　lewp.【\(\text{lewp} ( X ) = \{ \langle x , \{ x \} \rangle \mid x \in X \}\)】
準備　newp.【\(\text{newp} ( X , f ) = \{ x \in X \mid x \notin f ( x ) \}\)】
`f in X -> (wp X) and x in X ==> newp (X , f) #/=s f ap (x)` / W. ＜ pr0 ,, mapon0 OK
`f in X -> (wp X) ==> not {exi x in X . newp (X , f) =s f ap (x)}` / W. ＜ pr0 ,, mapon0 なぜだめ?

1 - b 順序対、写像

b1

順序対