e1

代数の始まり…

2項関数に対する1項述語

abbr …【\(( X , \mathop{{\sf f}} ) \, {:}\, \underline{2}\)】≈【\(\forall x , y \in X . x \mathop{{\sf f}} y \in X\)
$X #P$..f $X sub_ $X としたいが…?
abbr …【\(( X , \mathop{{\sf f}} ) \, {:}\, \text{C}\)】≈【\(\forall x , y \in X . x \mathop{{\sf f}} y = y \mathop{{\sf f}} x\)
abbr …【\(( X , \mathop{{\sf f}} ) \, {:}\, \text{A}\)】≈【\(\forall x , y , z \in X . x \mathop{{\sf f}} \, ( y \mathop{{\sf f}} z ) = ( x \mathop{{\sf f}} y ) \mathop{{\sf f}} z\)
abbr …【\(( X , \mathop{{\sf f}} ) \, {:}\, \text{J}\)】≈【\(\forall x \in X . x \mathop{{\sf f}} x = x\)

代数の最初の例にべき集合があります。証明においては = → =s が必要になります。
\(( \wp X , \cup ) \, {:}\, \underline{2} \text{C} \text{A} \text{J}\)\(\blacktriangleleft\)
\(( \wp X , \cap ) \, {:}\, \underline{2} \text{C} \text{A} \text{J}\)\(\blacktriangleleft\)
\(( \mathbb{M} , + ) \, {:}\, \underline{2} \text{C} \text{A}\)\(\blacktriangleleft\)
M*【\(( \mathbb{M} , \cdot ) \, {:}\, \underline{2} \text{C} \text{A}\)
\(( \wp ( X \times X ) , \circ ) \, {:}\, \underline{2} \text{A}\)\(\blacktriangleleft\)

2項関数の単位元

abbr …【\(\text{unit} ( X , \mathop{{\sf f}} )\)】≈【\(\{ e \mid \forall x \in X . e \, \mathop{{\sf f}} \, x = x = x \mathop{{\sf f}} e \}\)
\(\emptyset \in \text{unit} ( \wp X , \cup )\)\(\blacktriangleleft\)
\(X \in \text{unit} ( \wp X , \cap )\)\(\blacktriangleleft\)

e2

1以上の自然数

word(,s) … \(\mathbb{N}\)  
\N._【\(\mathbb{N} = \mathbb{M} \mathop\setminus 1\)
\N..【\(\mathbb{N} = \mathbb{M} \textit{+1}\)\(\blacktriangleleft\)
準備 M_n.【\(M_n = \{ n \in \mathbb{M} \mid n \neq 0 \Rightarrow \exists k \in \mathbb{M} . n = k \textit{+1} \}\)

この定理はいらない気が…

整数

word(s,s) … \(-\)  \(-\)  
-_.【\(- \,^\star{=}\; {-}\)
suc-【\(n \in \mathbb{N} \Longrightarrow ( - n ) \textit{+1} = - ( \bigcup n )\)

word(,s) … \(\mathbb{Z}\)  
整数は0以上のものと負のものに分けられるという定義を使うときは \Zm ≅ \Z を使用します。
\Zm.【\(\mathbb{Z} = \mathbb{M} \cup ( - \mathbb{N} )\)

整数の加法

+\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}\)
\(+\M\)
\(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で導入すべし

整数の乗法

*\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}\)
*\M_unit【\(1 \in \text{unit} \mathbb{M} , \cdot\)\(\blacktriangleleft\)

*を+より優先。precedを変える

e3

同値関係による商

有理数