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}\)】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}\)】
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} \}\)】
\({\cup}\text{F}\)【\(( \wp X , \cup ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A} \mathfrak{J}\)】\(\,{\blacktriangleleft}\,\)
\({\cup}\text{unit}\)【\(\emptyset \in \text{unit} ( \wp X , \cup )\)】\(\,{\blacktriangleleft}\,\)
\({\cap}\text{F}\)【\(( \wp X , \cap ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A} \mathfrak{J}\)】\(\,{\blacktriangleleft}\,\)
\({\cap}\text{unit}\)【\(X \in \text{unit} ( \wp X , \cap )\)】\(\,{\blacktriangleleft}\,\)
\({\circ}\text{F}\)【\(( \wp ( \widehat{\times} X ) , \circ ) \, {:}\, \underline{2} \mathfrak{A}\)】\(\,{\blacktriangleleft}\,\mathbb{W}.\)
alias = のせいで証明できなくなった
{% X ; [2 => A]}
自然数の演算
\(\mathbb{M}{+}\)【\(( \mathbb{M} , + ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A}\)】word(ss,s) … \(\cdot\)
\(\cdot 1\)【\(m \in \mathbb{M} \Longrightarrow m \cdot 1 = m\)】
\(\mathbb{M}{\cdot}\)【\(( \mathbb{M} , \cdot ) \, {:}\, \underline{2} \mathfrak{C} \mathfrak{A}\)】