順序対の話から始めます。\(\dagger\)
その最初の使用例として、置換公理の簡潔な記述を与えます。
順序対の集合は関係と呼ばれます。特別な関係として写像を定義します。\(\dagger\)
最後に「２つの集合の濃度が等しいか？」ということを議論します。\(\dagger\)
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\)
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 ) ) )\)
対集合公理は他の公理から導出されます。未完！
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\)
cvt … \(\stackrel{\text{^}}{\mathop{{\sf f}}} A\) ≃ \(\{ \mathop{{\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{^*}}{\mathop{{\sf f}}} b\) ≃ \(\{ a \mathop{{\sf f}} b \mid a \in A \}\)
cvt … \(a \stackrel{\text{*^}}{\mathop{{\sf f}}} B\) ≃ \(\{ a \mathop{{\sf f}} b \mid b \in B \}\)
cvt … \(A \stackrel{\text{^^}}{\mathop{{\sf f}}} B\) ≃ \(\{ a \mathop{{\sf f}} b \mid a \in A , b \in B \}\)
ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \forall X \, \dot\exists ( X \cap C )\)
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\)
分出公理は置換公理から導出されます。未完！
Rel. … \(\text{Rel} = \{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\)
word(ss,s) … \(\times\)
pr^^. {pr^^ **=_ {^^}pr}
word(s,s)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 \}\)
\(R \in \text{Rel} \Longrightarrow \triangleleft ( R ) = { \stackrel{\text{^}}{\triangleleft} } R , \triangleright ( R ) = { \stackrel{\text{^}}{\triangleright} } R\) \(\blacktriangleleft\)
\(\text{Rel} = \{ R \mid R \subset \triangleleft ( R ) \times \triangleright ( R ) \}\) \(\blacktriangleleft\)
定義域の制限
word(ss,s) … \(|\)
rest. … \(R | _ X = \{ \langle x , y \rangle \in R \mid x \in X \}\)
pr<!. … \(\triangleleft! ( f ) = \{ x \mid \exists! y \, \langle x , y \rangle \in f \}\)
=% ≅ =
word(ss,s) … ap
ap.' … \(x \in \triangleleft! ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)
ap0 … \(x \in \triangleleft! ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\) \(\blacktriangleleft\)
word(ss,s) … ap_
ap_. {ap_ {**}=_ ap__}
ap_0 … \(A \subset \triangleleft! ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\) \(\blacktriangleleft\)
swI … \(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\) \(\blacktriangleleft\)
word(s,s) … \(^\leftrightarrow\)
sw_. … \(^\leftrightarrow \stackrel{\star\!\star}{=} \stackrel{\text{^^}}{^\leftrightarrow}\)
sw_0 … \(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\) \(\blacktriangleleft\)
sw_I … \(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\) \(\blacktriangleleft\)
comp. … \(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)
comp0 … \(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\) \(\blacktriangleleft\)
compA … \( R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\) \(\blacktriangleleft\)
compX … \( R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\) \(\blacktriangleleft\)
comp_ap … \(x \in \triangleleft! ( f ) , f ( x ) \in \triangleleft! ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\) \(\blacktriangleleft\)
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 \triangleleft ( f ) = X \}\)
\( f , g \in \text{mapon} ( X ) \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\) \(\blacktriangleleft\)
壊れた。たぶんmaponを変えたせい
一項関数の制限により写像が作られます。ただしクラスであることに注意。
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\)
->. … \(X \to Y = \{ f \subset X \times Y \mid X \subset \triangleleft! ( f ) \}\)
->..' … \(X \to Y = \{ f \in \text{mapon} ( X ) \mid \triangleright ( 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 \triangleleft ( f ) \to \triangleright ( f ) \} = \{ f \mid \exists X \exists Y f \in X \to Y \}\) \(\blacktriangleleft\)
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\)
->I.' … \(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \triangleright ( f ) \to X \}\)
->S.' … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \triangleright ( 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\)
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\)
=#.' … \(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 \stackrel{{\tt /}}{\stackrel{\#}=} Y\)
=#0 … \(X \stackrel{\#}= \emptyset \Longleftrightarrow X = \emptyset\) \(\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 \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 なぜだめ?
その最初の使用例として、置換公理の簡潔な記述を与えます。
順序対の集合は関係と呼ばれます。特別な関係として写像を定義します。\(\dagger\)
最後に「２つの集合の濃度が等しいか？」ということを議論します。\(\dagger\)
b1
順序対
word(ss,s) … prword(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\)
置換公理
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 ) ) )\)
対集合公理は他の公理から導出されます。未完！
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\)
関数の像
word(s,s→s,c) … \(\text{^}\)cvt … \(\stackrel{\text{^}}{\mathop{{\sf f}}} A\) ≃ \(\{ \mathop{{\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{^*}}{\mathop{{\sf f}}} b\) ≃ \(\{ a \mathop{{\sf f}} b \mid a \in A \}\)
cvt … \(a \stackrel{\text{*^}}{\mathop{{\sf f}}} B\) ≃ \(\{ a \mathop{{\sf f}} b \mid b \in B \}\)
cvt … \(A \stackrel{\text{^^}}{\mathop{{\sf f}}} B\) ≃ \(\{ a \mathop{{\sf f}} b \mid a \in A , b \in B \}\)
分出公理
word(c,p) … \(\text{ax_s}\)ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \forall X \, \dot\exists ( X \cap C )\)
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\)
分出公理は置換公理から導出されます。未完！
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^^ **=_ {^^}pr}
word(s,s)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 \}\)
\(R \in \text{Rel} \Longrightarrow \triangleleft ( R ) = { \stackrel{\text{^}}{\triangleleft} } R , \triangleright ( R ) = { \stackrel{\text{^}}{\triangleright} } R\) \(\blacktriangleleft\)
\(\text{Rel} = \{ R \mid R \subset \triangleleft ( R ) \times \triangleright ( R ) \}\) \(\blacktriangleleft\)
定義域の制限
word(ss,s) … \(|\)
rest. … \(R | _ X = \{ \langle x , y \rangle \in R \mid x \in X \}\)
代入
word(s,s) … \(\triangleleft!\)pr<!. … \(\triangleleft! ( f ) = \{ x \mid \exists! y \, \langle x , y \rangle \in f \}\)
=% ≅ =
word(ss,s) … ap
ap.' … \(x \in \triangleleft! ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)
ap0 … \(x \in \triangleleft! ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\) \(\blacktriangleleft\)
word(ss,s) … ap_
ap_. {ap_ {**}=_ ap__}
ap_0 … \(A \subset \triangleleft! ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\) \(\blacktriangleleft\)
成分の入れ替え
sw. … \(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)swI … \(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\) \(\blacktriangleleft\)
word(s,s) … \(^\leftrightarrow\)
sw_. … \(^\leftrightarrow \stackrel{\star\!\star}{=} \stackrel{\text{^^}}{^\leftrightarrow}\)
sw_0 … \(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\) \(\blacktriangleleft\)
sw_I … \(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\) \(\blacktriangleleft\)
合成
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 ) \}\)
comp0 … \(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\) \(\blacktriangleleft\)
compA … \( R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\) \(\blacktriangleleft\)
compX … \( R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\) \(\blacktriangleleft\)
comp_ap … \(x \in \triangleleft! ( f ) , f ( x ) \in \triangleleft! ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\) \(\blacktriangleleft\)
b3
写像①
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 \triangleleft ( f ) = X \}\)
\( f , g \in \text{mapon} ( X ) \Longrightarrow f = g \Leftrightarrow \forall x \in X . f ( x ) = g ( x )\) \(\blacktriangleleft\)
壊れた。たぶんmaponを変えたせい
一項関数の制限により写像が作られます。ただしクラスであることに注意。
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 \triangleleft! ( f ) \}\)
->..' … \(X \to Y = \{ f \in \text{mapon} ( X ) \mid \triangleright ( 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 \triangleleft ( f ) \to \triangleright ( 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 \triangleright ( f ) \to X \}\)
->S.' … \(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \triangleright ( 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 \stackrel{{\tt /}}{\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 なぜだめ?