1 - c1
対も基本的ですが定義は与えられません。\(\langle x,y\rangle=\{x,\{x,y\}\}\) とはしません。
後に、対の集合として写像が作られますが、別種の対が写像として作られます。
対、直積
word(ss,s) … pr abbr …【\(\langle x , y \rangle\)】≈ 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}\,\)
word(ss,s) … \(\times\)
\({\times}.\) {pr_ **=_ #Ppr}
対の集合は関係と呼ばれます。特別な関係に写像があります。
word(,c)F … \(\text{Rel}\)
cvt …【\(\text{Rel}\)】≃【\(\{ R \mid \forall x \in R . x = \langle \triangleleft x , \triangleright x \rangle \}\)】
%をprに
定義域、値域
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 \}\)】
【\(\text{Rel} = \{ R \mid R \subset \text{dom} ( R ) \times \text{im} ( R ) \}\)】\(\,{\blacktriangleleft}\,\)
定義域の制限や像は写像に対してよく使用されます。
word(ss,s) … rest abbr …【\(f | _{ X }\)】≈ rest (f) (X)
rest.【\(R | _{ X } = \{ \langle x , y \rangle \in R \mid x \in X \}\)】
word(ss,s) … ap_
ap_.【\(R ( A ) = \{ y \mid \exists a \in A . \langle a , y \rangle \in R \}\)】
代入
word(s,s) … \(\text{dom!}\)dom!.【\(\text{dom!} ( f ) = \{ x \mid \exists! y \, \langle x , y \rangle \in f \}\)】
=% ≅ =
word(ss,s)F … ap
=%.【\(x \in \text{dom!} ( f ) \Longrightarrow y = f ( x ) \Leftrightarrow \langle x , y \rangle \in f\)】
ap0【\(x \in \text{dom!} ( f ) \Longrightarrow \langle x , f ( x ) \rangle \in f\)】\(\,{\blacktriangleleft}\,\)
ap_0【\(A \subset \text{dom!} ( f ) \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\)】\(\,{\blacktriangleleft}\,\)
成分の入れ替え
word(s,s) … \(^\leftrightarrow\)sw.【\(\langle x , y \rangle ^\leftrightarrow = \langle y , x \rangle\)】
sw巾【\(\langle x , y \rangle ^\leftrightarrow \, \! ^\leftrightarrow = \langle x , y \rangle\)】\(\,{\blacktriangleleft}\,\)
word(s,s) … \(^\leftrightarrow\)
sw_.【\(^\leftrightarrow \,^{\star\!\star}{=}\; {^\leftrightarrow}\)】
sw_0【\(R \subset X \times Y \Longrightarrow R ^\leftrightarrow \subset Y \times X\)】\(\,{\blacktriangleleft}\,\)
sw_巾【\(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 ) \}\)】
compRel【\(R \subset X \times Y , S \subset Y \times Z \Longrightarrow S \circ R \subset X \times Z\)】\(\,{\blacktriangleleft}\,\)
comp_A【\( R , S , T \in \text{Rel} \Longrightarrow ( T \circ S ) \circ R = T \circ ( S \circ R )\)】\(\,{\blacktriangleleft}\,\)
comp逆【\( R , S \in \text{Rel} \Longrightarrow ( R \circ S ) ^\leftrightarrow = S ^\leftrightarrow \circ R ^\leftrightarrow\)】\(\,{\blacktriangleleft}\,\)
comp_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\)map.【\(X \to Y = \{ f \subset X \times Y \mid X \subset \text{dom!} ( f ) \}\)】
map..【\(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}\,\)
comp_map【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\)】\(\,{\blacktriangleleft}\,\)
rest_map【\(f \in X \to Y \Longrightarrow f | _{ A } \in X \cap A \to Y\)】\(\,{\blacktriangleleft}\,\)
word(s,c) … \(\text{mapon} \)
cvt …【\(\text{mapon} ( X )\)】≃【\(\{ f \mid \exists Y \, f \in X \to Y \}\)】
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\)map:I._【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in \text{im} ( f ) \to X \}\)】\(\,{\triangleleft}\,\)
map:S._【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{im} ( f ) = Y \}\)】\(\,{\triangleleft}\,\)
map:IS.【\(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)】
map:IS..【\(X \stackrel{\rm IS}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in Y \to X \}\)】\(\,{\blacktriangleleft}\,\)
mapon1【\(f \in \text{mapon} ( X ) \Longrightarrow f \in X \stackrel{\rm S}\to \text{im} ( f )\)】\(\,{\blacktriangleleft}\,\)
map: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}\,\)
map: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}\,\)
comp_map:I【\(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}\,\)
comp_map:S【\(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}\,\)
comp_map:IS【\(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}\,\)一点集合への写像
map:IS0【\(\{ \langle x , y \rangle \} \in \{ x \} \stackrel{\rm IS}\to \{ y \}\)】\(\,{\blacktriangleleft}\,\)
word(ss,s) … on abbr …【\(f _{ \mid X }\)】≈ on (X) (f)
on.【\(y _{ \mid X } = X \times \{ y \}\)】
on0【\(X \to \{ y \} = \{ y _{ \mid X } \}\)】\(\,{\blacktriangleleft}\,\)
onは入力補助を？
互換
word(ss,s) … \(\leftrightharpoons\)
exc.【\(x \leftrightharpoons y = \{ \langle x , y \rangle , \langle y , x \rangle \}\)】
exc0【\(x \leftrightharpoons y \in \{ x , y \} \stackrel{\rm IS}\to \{ x , y \}\)】\(\,{\blacktriangleleft}\,\)
恒等写像
word(s,s) … \(\text{id}\)id.【\(\text{id} _ X = \{ \langle x , x \rangle \mid x \in X \}\)】
id0【\(\text{id} _ X \in X \stackrel{\rm IS}\to X\)】\(\,{\blacktriangleleft}\,\)
comp単【\(R \subset X \times Y \Longrightarrow \text{id} Y \circ R = R = R \circ \text{id} X\)】\(\,{\blacktriangleleft}\,\)
rest_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{\#}<\)=#._【\(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)】\(\,{\triangleleft}\,\)
<=#._【\(X \stackrel{\#}\le Y \Longleftrightarrow X \stackrel{\rm I}\to Y \neq \emptyset\)】\(\,{\triangleleft}\,\)
<#.【\(X \stackrel{\#}< Y \Longleftrightarrow X \stackrel{\#}\le Y , X \cancel{\stackrel{\#}=} Y\)】
=#ITX【\(\stackrel{\#}= {:}\, \mathfrak{I} \mathfrak{T} \mathfrak{X}\)】\(\,{\blacktriangleleft}\,\)
<=#IT【\(\stackrel{\#}\le {:}\, \mathfrak{I} \mathfrak{T}\)】\(\,{\blacktriangleleft}\,\)
【\(X \subset Y \Rightarrow X \stackrel{\#}\le Y\)】\(\,{\blacktriangleleft}\,\)
未<#T【\(( X \stackrel{\#}< Y \stackrel{\#}\le Z ) \mathbin{\rm o\!r} ( X \stackrel{\#}\le Y \stackrel{\#}< Z ) \Longrightarrow X \stackrel{\#}< Z\)】\(\,{\blacktriangleleft}\,\)
有限の濃度
=#0【\(X \stackrel{\#}= 0 \Longleftrightarrow X = \emptyset\)】\(\,{\blacktriangleleft}\,\)=#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}\) \VInf
cvt …【\(\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}\,\)
cvt …【\(\mathbb{V}_\infty\)】≃【\(\mathop\setminus \mathbb{V}_{\not\infty}\)】
有限の計算
直和の濃度【\( m , n \in \mathbb{M} \Longrightarrow ( 1 m ) \cup ( n 1 ) \stackrel{\#}= m + n\)】\(\,{\blacktriangleleft}\,\)
集合の直和作る？
\(m+n = \{0\}\times m \cup \{1\}\times n\)