1 - d1
代数の始まり…
2項関数に対する1項述語
abbr …【\(( {\sf X} , \mathop{{\sf f}} ) \, {:}\, \underline{2}\)】≈【\(\forall {\sf x} , {\sf y} \in {\sf X} . {\sf x} \mathop{{\sf f}} {\sf y} \in {\sf X}\)】$X #P$..f $X sub_ $X としたいが…？
abbr …【\(( {\sf X} , \mathop{{\sf f}} ) \, {:}\, \mathfrak{C}\)】≈【\(\forall {\sf x} , {\sf y} \in {\sf X} . {\sf x} \mathop{{\sf f}} {\sf y} = {\sf y} \mathop{{\sf f}} {\sf x}\)】
abbr …【\(( {\sf X} , \mathop{{\sf f}} ) \, {:}\, \mathfrak{A}\)】≈【\(\forall {\sf x} , {\sf y} , {\sf z} \in {\sf X} . {\sf x} \mathop{{\sf f}} \, ( {\sf y} \mathop{{\sf f}} {\sf z} ) = ( {\sf x} \mathop{{\sf f}} {\sf y} ) \mathop{{\sf f}} {\sf z}\)】
abbr …【\(( {\sf X} , \mathop{{\sf f}} ) \, {:}\, \mathfrak{J}\)】≈【\(\forall {\sf x} \in {\sf X} . {\sf x} \mathop{{\sf f}} {\sf x} = {\sf x}\)】
代数の最初の例にべき集合があります。証明においては = → =s が必要になります。
【\(( \wp X , \cup ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A} \mathfrak{J}\)】\(\,{\blacktriangleleft}\,\)
【\(( \wp X , \cap ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A} \mathfrak{J}\)】\(\,{\blacktriangleleft}\,\)
【\(( \mathbb{M} , + ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A}\)】\(\,{\blacktriangleleft}\,\)
\(\mathbb{M}{\cdot}\)【\(( \mathbb{M} , \cdot ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A}\)】
【\(( \wp ( X \times X ) , \circ ) \, {:}\, \underline{2} \mathfrak{A}\)】\(\,{\blacktriangleleft}\,\)
alias = のせいで証明できなくなった
2項関数の単位元
abbr …【\(\text{unit} ( {\sf X} , \mathop{{\sf f}} )\)】≈【\(\{ {\sf e} \mid \forall {\sf x} \in {\sf X} . {\sf e} \, \mathop{{\sf f}} \, {\sf x} = {\sf x} = {\sf x} \mathop{{\sf f}} {\sf e} \}\)】【\(\emptyset \in \text{unit} ( \wp X , \cup )\)】\(\,{\blacktriangleleft}\,\)
【\(X \in \text{unit} ( \wp X , \cap )\)】\(\,{\blacktriangleleft}\,\)
1 - d2
整数
word(s,s) … \(-\) \(-\)\({-}\_.\)【\(- \,^\star{=}\; {-}\)】
\(\text{suc-}\)【\(n \in \mathbb{N} \Longrightarrow ( - n ) \textit{+1} = - ( \bigcup n )\)】
word(,s) … \(\mathbb{Z}\)
整数は0以上のものと負のものに分けられるという定義を使うときは \Zm ≅ \Z を使用します。
\(\mathbb{Z}.\)【\(\mathbb{Z} = \mathbb{M} \cup ( - \mathbb{N} )\)】
整数の加法
\({+}_\mathbb{Z}\)【\(\begin{cases} m \in \mathbb{Z} \Longrightarrow m + 0 = m \\ m \in \mathbb{Z} , \; n \in \mathbb{M} \Longrightarrow m + ( n \textit{+1} ) = ( m + n ) \textit{+1} , m + ( - n ) = - ( - m + n ) \end{cases}\)】\({+}_\mathbb{M}\,{\blacktriangleleft}\,\)
【\(m \in \mathbb{Z} \Longrightarrow m + 1 = m \textit{+1}\)】\(\,{\blacktriangleleft}\,\)
【\(n \in \mathbb{Z} \Longrightarrow 0 + n = n\)】\(\,{\blacktriangleleft}\,\)
準備 \(M_{-u}.\)【\(M_{-u} = \{ n \in \mathbb{M} \mid 0 + ( - n ) = - n \}\)】
【\(0 \in \text{unit} ( \mathbb{Z} , + )\)】\(\,{\blacktriangleleft}\,\)
+の性質をいろいろ？
m-nをabbrで導入すべし
整数の乗法
\({\cdot}_\mathbb{Z}\)【\(\begin{cases} m \in \mathbb{Z} \Longrightarrow m \cdot 0 = 0 \\ m \in \mathbb{Z} , n \in \mathbb{M} \Longrightarrow m \cdot ( n \textit{+1} ) = ( m \cdot n ) + m , \; m \cdot ( - n ) = - m \cdot n \end{cases}\)】\({*}_\mathbb{M}\text{unit}\)【\(1 \in \text{unit} ( \mathbb{M} , \cdot )\)】\(\,{\blacktriangleleft}\,\)
*を+より優先。precedを変える
1 - d3
部分集合の全体はべき集合と呼ばれます。べき集合の基本的な性質を調べます。
べき集合
word(s,s) … \(\wp\)\(\wp.\)【\(\wp X = \{ A \mid A \subset X \}\)】
【\(\wp \emptyset = \{ \emptyset \}\)】\(\,{\blacktriangleleft}\,\)
【\(\wp ( \{ x \} ) = \{ \emptyset , \{ x \} \}\)】\(\,{\blacktriangleleft}\,\)
べき集合の濃度
Cantorの定理\({\stackrel{\#}<}\wp\)【\(X \stackrel{\#}< \wp X\)】\(\,{\blacktriangleleft}\,\)
準備 \(\text{lewp}.\)【\(\text{lewp} ( X ) = \{ \langle x , \{ x \} \rangle \mid x \in X \}\)】
準備 \(\text{newp}.\)【\(\text{newp} ( X , f ) = \{ x \in X \mid x \notin f ( x ) \}\)】
`f in X map (wp X) and x in X ==> newp (X , f) #/=s {ap f ; x}` / W. ＜ %0，mapon0 OK
`f in X map (wp X) ==> not {exi x in X . newp (X , f) =s {ap f ; x}}` / W. ＜ %0，mapon0 なぜだめ?
\({\stackrel{\#}=}\wp\)【\(\wp X \stackrel{\#}= X \to 2\)】
準備 \(\text{wp2}.\)【\(\text{wp2} ( X ) = \{ \langle A , f \rangle \mid A \in \wp X , f = a \}\)】
有限部分集合の全体
word(s,s) … \(\wp_{\not\infty}\)\(\wp_{\not\infty}.\)【\(\wp_{\not\infty} ( X ) = \wp ( X ) \cap \mathbb{V}_{\not\infty}\)】
【\(\wp_{\not\infty} ( \mathbb{M} ) \stackrel{\#}= \mathbb{M}\)】