1 - c1
対も基本的ですが定義は与えられません。\(\langle x,y\rangle=\{x,\{x,y\}\}\) とはしません。
後に、対の集合として写像が作られますが、別種の対が写像として作られます。
対、直積
word(ss,s) … % abbr …【\(\langle {\sf X} , {\sf Y} \rangle\)】≈ % $X $Y次のものは対の成分を取り出します。
word(s,s) … \(\triangleleft\) \(\triangleright\)
\({\triangleleft.}\)【\(\triangleleft \langle x , y \rangle = x\)】
\({\triangleright.}\)【\(\triangleright \langle x , y \rangle = y\)】
\(\text{%0}\)【\(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\)】\(\,{\blacktriangleleft}\,\)
word(ss,s) … \(\times\)
\({\times}.\) {%_ **=_ #P%}
対の集合は関係と呼ばれます。特別な関係に写像があります。
word(,c) … \(\text{Rel}\)
def …【\(\text{Rel}\)】≃【\(\{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\)】
定義域、値域
word(s,s) … \(\text{dom}\) \(\text{im}\)\(\text{dom.}\)【\(\text{dom} ( R ) = \{ x \mid \exists y \, \langle x , y \rangle \in R \}\)】
\(\text{im.}\)【\(\text{im} ( R ) = \{ y \mid \exists x \, \langle x , y \rangle \in R \}\)】
【\(\text{Rel} = \{ R \mid R \subset \text{dom} ( R ) \times \text{im} ( R ) \}\)】\(\,{\blacktriangleleft}\,\)
定義域の制限や像は写像に対してよく使用されます。
word(ss,s) … rest abbr …【\({\sf F} | _{ {\sf X} }\)】≈ rest $F $X
\(|.\)【\(R | _{ X } = \{ \langle x , y \rangle \in R \mid x \in X \}\)】
word(ss,s) … ap_ abbr …【\({\sf P} ( {\sf A} )\)】≈ ap_ $P $A
\(\text{ap_}.\)【\(R ( A ) = \{ y \mid \exists a \in A . \langle a , y \rangle \in R \}\)】
代入
word(s,s) … \(\text{dom!}\)\(\text{dom!}.\)【\(\text{dom!} ( f ) = \{ x \mid \exists! y \, \langle x , y \rangle \in f \}\)】
=% ≅ =
word(ss,s) … ap abbr …【\({\sf F} ( {\sf X} )\)】≈ ap $F $X
\({=}.\)【\(x \in \text{dom!} ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)】
\(\text{ap0}\)【\(x \in \text{dom!} ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\)】\(\,{\blacktriangleleft}\,\)
\(\text{ap_0}\)【\(A \subset \text{dom!} ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\)】\(\,{\blacktriangleleft}\,\)
成分の入れ替え
word(s,s) … \(^\leftrightarrow\)\(\text{sw.}\)【\(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)】
\(\text{sw}巾\)【\(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\)】\(\,{\blacktriangleleft}\,\)
word(s,s) … \(^\leftrightarrow\)
\(\text{sw_.}\)【\(^\leftrightarrow \,^{\star\!\star}{=}\; {^\leftrightarrow}\)】
\(\text{sw_0}\)【\(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\)】\(\,{\blacktriangleleft}\,\)
\(\text{sw_}巾\)【\(R \in \text{Rel} \Longrightarrow R ^\leftrightarrow \, \! ^\leftrightarrow = R\)】\(\,{\blacktriangleleft}\,\)
合成
word(ss,s) … \(\circ\)\({\circ}.\)【\(S \circ R = \{ \langle x , z \rangle \mid \exists y \, ( \langle x , y \rangle \in R , \langle y , z \rangle \in S ) \}\)】
\({\circ}\text{Rel}\)【\(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\)】\(\,{\blacktriangleleft}\,\)
\({\circ}\mathfrak{A} \)【\( R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\)】\(\,{\blacktriangleleft}\,\)
\({\circ}逆\)【\( R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\)】\(\,{\blacktriangleleft}\,\)
\({\circ}\text{ap}\)【\(x \in \text{dom!} ( f ) , f ( x ) \in \text{dom!} ( g ) \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\)】\(\,{\blacktriangleleft}\,\)
1 - c2
写像とは「集合の各元を他の集合の元にそれぞれ対応させるもの」ですが、以下にあるような定義が採用されます。基本的な写像の例も紹介されます。
写像
word(ss,s) … \(\to\)\({\to}.\)【\(X \to Y = \{ f \subset X \times Y \mid X \subset \text{dom!} ( f ) \}\)】
\({\to}{.}{.}\)【\(X \to Y = \{ f \mid f = \{ \langle x , f ( x ) \rangle \mid x \in X \} , \forall x \in X . f ( x ) \in Y \}\)】\(\,{\blacktriangleleft}\,\)
【\(f \in \text{dom} ( f ) \to \text{im} ( f ) \Longleftrightarrow f \in \text{Rel} , \text{dom} ( f ) \subset \text{dom!} ( f )\)】\(\,{\blacktriangleleft}\,\)
\({\circ}{\to}\)【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\)】\(\,{\blacktriangleleft}\,\)
\(|{\to}\)【\(f \in X \to Y \Longrightarrow f | _{ A } \in X \cap A \to Y\)】\(\,{\blacktriangleleft}\,\)
word(s,c) … \(\text{mapon} \)
def …【\(\text{mapon} ( {\sf X} )\)】≃【\(\{ {\sf f} \mid \exists {\sf y} \, {\sf f} \in {\sf X} \to {\sf y} \}\)】
\(\text{mapon0}\)【\(f \in \text{mapon} ( X ) \Longrightarrow f = \{ \langle x , f ( x ) \rangle \mid x \in X \}\)】\(\,{\blacktriangleleft}\,\)
【\(\text{mapon} ( \emptyset ) = \{ \emptyset \}\)】\(\,{\blacktriangleleft}\,\)
mapon0逆も？
単射、全射
word(ss,s) … \(\stackrel{\rm I}\to\) \(\stackrel{\rm S}\to\) \(\stackrel{\rm IS}\to\)\({\stackrel{\rm I}\to}.\)【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \text{im} ( f ) \to X \}\)】\(\,{\triangleleft}\,\)
\({\stackrel{\rm S}\to}.\)【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{im} ( f ) = Y \}\)】\(\,{\triangleleft}\,\)
\({\stackrel{\rm IS}\to}.\)【\(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)】
\({\stackrel{\rm IS}\to}{.}{.}\)【\(X \stackrel{\rm IS}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in Y \to X \}\)】\(\,{\blacktriangleleft}\,\)
\(\text{mapon1}\)【\(f \in \text{mapon} ( X ) \Longrightarrow f \in X \stackrel{\rm S}\to \text{im} ( f )\)】\(\,{\blacktriangleleft}\,\)
\({\stackrel{\rm I}\to}{.}{.}\)【\(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}\,\)
\({\stackrel{\rm S}\to}{.}{.}\)【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \forall y \in Y . \exists x \in X . y = f ( x ) \}\)】\(\,{\blacktriangleleft}\,\)
\({\circ}{\stackrel{\rm I}\to}\)【\(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}\,\)
\({\circ}{\stackrel{\rm S}\to}\)【\(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}\,\)
\({\circ}{\stackrel{\rm IS}\to}\)【\(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}\,\)
小さい集合への写像
【\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\)】\(\,{\blacktriangleleft}\,\)一点集合への写像
\({\stackrel{\rm IS}\to}0\)【\(\{ \langle x , y \rangle \} \in \{ x \} \stackrel{\rm IS}\to \{ y \}\)】\(\,{\blacktriangleleft}\,\)
word(ss,s) … on abbr …【\({\sf Y} _{ \mid {\sf X} }\)】≈ on $X $Y
\(\text{on.}\)【\(y _{ \mid X } = X \times \{ y \}\)】
\(\text{on0}\)【\(X \to \{ y \} = \{ y _{ \mid X } \}\)】\(\,{\blacktriangleleft}\,\)
onは入力補助を？
互換
word(ss,s) … \(\leftrightharpoons\)
\({\leftrightharpoons}.\)【\(x \leftrightharpoons y = \{ \langle x , y \rangle , \langle y , x \rangle \}\)】
\({\leftrightharpoons}0\)【\(x \leftrightharpoons y \in \{ x , y \} \stackrel{\rm IS}\to \{ x , y \}\)】\(\,{\blacktriangleleft}\,\)
恒等写像
word(s,s) … id abbr …【\(\text{id} _{ {\sf X} }\)】≈ id $X\(\text{id}.\)【\(\text{id} _{ X } = \{ \langle x , x \rangle \mid x \in X \}\)】
\(\text{id0}\)【\(\text{id} _{ X } \in X \stackrel{\rm IS}\to X\)】\(\,{\blacktriangleleft}\,\)
\({\circ}単\)【\(R \subset X \times Y \Longrightarrow \text{id} _{ Y } \circ R = R = R \circ \text{id} _{ X }\)】\(\,{\blacktriangleleft}\,\)
\(|\text{id}\)【\(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 } \}\)】\(\,{\blacktriangleleft}\,\)
【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid f \circ f ^\leftrightarrow = \text{id} _{ Y } \}\)】\(\,{\blacktriangleleft}\,\)
対、直積
aryというword
(擬)一項関数から作られる写像
word関数 … fs : (s,s)→(s,s)abbr … 【\({\sf F} _{ {\sf X} }\)】 ≈ fs $F $X
1 - c3
基数とかめんどくさいので濃度の定義もされません。「２つの集合の濃度が等しいか？」という事は議論されます。
濃度
word(ss,p) … \(\stackrel{\#}=\) \(\stackrel{\#}\le\) \(\stackrel{\#}<\)\(\stackrel{\#}=.\)【\(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)】\(\,{\triangleleft}\,\)
\(\stackrel{\#}\le.\)【\(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\)】\(\,{\triangleleft}\,\)
\(\stackrel{\#}<.\)【\(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \cancel{\stackrel{\#}=} Y\)】
\({\stackrel{\#}=}\text{ITX}\)【\(\stackrel{\#}= {:}\, \mathfrak{I} \mathfrak{T} \mathfrak{X}\)】\(\,{\blacktriangleleft}\,\)
\({\stackrel{\#}\le}\text{IT}\)【\(\stackrel{\#}\le {:}\, \mathfrak{I} \mathfrak{T}\)】\(\,{\blacktriangleleft}\,\)
【\(X \subset Y \Rightarrow X \stackrel{\#}\le Y\)】\(\,{\blacktriangleleft}\,\)
未\({\stackrel{\#}<}\text{T}\)【\(( X \stackrel{\#}< Y \stackrel{\#}\le Z ) \mathbin{\rm o\!r} ( X \stackrel{\#}\le Y \stackrel{\#}< Z ) \Longrightarrow X \stackrel{\#}< Z\)】\(\,{\blacktriangleleft}\,\)
有限の濃度
\({\stackrel{\#}=}0\)【\(X \stackrel{\#}= 0 \Longleftrightarrow X = \emptyset\)】\(\,{\blacktriangleleft}\,\)\({\stackrel{\#}=}1\)【\(X \stackrel{\#}= 1 \Longleftrightarrow \exists x \, X = \{ x \}\)】\(\,{\blacktriangleleft}\,\)
未\({\stackrel{\#}=}{\tt n}\)【\(X \stackrel{\#}= {\tt n} \Longleftrightarrow \exists^* x_{1} , \cdots , x_{\tt n} \, X = \{ x_{1} , \cdots , x_{\tt n} \}\)】\(\,{\blacktriangleleft}\,\)
`f in n map:S X => X =s {set {ap f ; 0} ; {ap f ; 1} ; … ; {ap f ; n-1}}` / map:S.. / map.. / W. ＜ n.
neq2 が必要なハズ。<=ではaryも
有限の計算
鳩の巣原理とか部屋割り論法と呼ばれる補題から。【\( m , n \in \mathbb{M} , m \stackrel{\#}\le n \Longrightarrow m \subset n\)】\(\,{\blacktriangleleft}\,\)
準備 \(F_a.\)【\(F_a = \{ n \in \mathbb{M} \mid \forall m \in \mathbb{M} . ( m \stackrel{\#}\le n \Rightarrow m \subset n ) \}\)】
`F_a in_ Ind` / W. &l ＜ `0 in \M`
【\( m , n \in \mathbb{M} , m \subsetneq n \Longrightarrow \not\exists f f \in m \stackrel{\rm S}\to n\)】\(\,{\blacktriangleleft}\,\)
【\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm I}\to n = n \stackrel{\rm IS}\to n\)】\(\,{\blacktriangleleft}\,\)
【\(n \in \mathbb{M} \Longrightarrow n \stackrel{\rm S}\to n = n \stackrel{\rm IS}\to n\)】\(\,{\blacktriangleleft}\,\)
集合を有限と無限に分けます。
word(,c) … \(\mathbb{V}_{\not\infty}\) \(\mathbb{V}_\infty\)
def …【\(\mathbb{V}_{\not\infty}\)】≃【\(\{ X \mid \exists n \in \mathbb{M} . X \stackrel{\#}= n \}\)】
【\(\mathbb{V}_{\not\infty} = \{ X \mid X \stackrel{\#}\le \mathbb{M} \}\)】\(\,{\blacktriangleleft}\,\)
def …【\(\mathbb{V}_\infty\)】≃【\(\mathop\setminus \mathbb{V}_{\not\infty}\)】
有限の計算
直和の濃度【\( m , n \in \mathbb{M} \Longrightarrow ( 1 \times m ) \cup ( n \times 1 ) \stackrel{\#}= m + n\)】\(\,{\blacktriangleleft}\,\)
集合の直和作る？
\(m+n = \{0\}\times m \cup \{1\}\times n\)