c1
対も基本的ですが定義は与えられません。\(\langle x,y\rangle=\{x,\{x,y\}\}\) とはしません。
後に、対の集合として写像が作られますが、別種の対が写像として作られます。
対、直積
word(ss,s)F … 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 \}\)】
定義域、値域
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.【\(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\)
c2
写像とは「集合の各元を他の集合の元にそれぞれ対応させるもの」ですが、以下にあるような定義が採用されます。基本的な写像の例も紹介されます。
内部での -> を使用をやめるので map を -> にできるハズ
写像
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 \}\)】
map:S._【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{im} ( f ) = Y \}\)】
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.【\(y | _ X = X \times \{ y \}\)】
on0【\(X \to \{ y \} = \{ y | _ X \}\)】\(\blacktriangleleft\)
互換
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\)
【\(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} _ X\)】 ≈ fs $F X
c3
基数とかめんどくさいので濃度の定義もされません。「２つの集合の濃度が等しいか？」という事は議論されます。
濃度
word(ss,p) … \(\stackrel{\#}=\) \(\stackrel{\#}\le\) \(\stackrel{\#}<\)=#._【\(X \stackrel{\#}= Y \Longleftrightarrow X \stackrel{\rm IS}\to Y \neq \emptyset\)】
<=#._【\(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\)】
=#ITX【\(\stackrel{\#}= {:}\, \text{I} \text{T} \text{X}\)】\(\blacktriangleleft\)
<=#IT【\(\stackrel{\#}\le {:}\, \text{I} \text{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}\) \(\mathbb{V}_\infty\)
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 \times m ) \cup ( n \times 1 ) \stackrel{\#}= m + n\)】\(\blacktriangleleft\)
集合の直和作る？
\(m+n = \{0\}\times m \cup \{1\}\times n\)