1 演算に関する定理

\(\mathbb{W}\)(ss,s) … \(+\)
一般結合則について少し厳密に述べてみます。
\(a , b \in \{ x \mid \forall y , z \; x + ( y + z ) = ( x + y ) + z \} \Longrightarrow a + ( b + ( y + z ) ) = ( ( a + b ) + y ) + z\) \(\blacktriangleleft\) O

演算の中心について。\(+\) が結合的なら、可換なものどうしの和もまた可換です。
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow ( a , b \in \{ x \mid \forall y \, x + y = y + x \} \Longrightarrow a + b \in \{ x \mid \forall y \, x + y = y + x \} )\) \(\blacktriangleleft\) O

\(\mathrm{C}\) … \(\{ x \mid \forall y \, x + y = y + x \}\)
\(\forall u , v , w \; u + ( v + w ) = ( u + v ) + w \Longrightarrow a , b \in \mathrm{C} \Rightarrow a + b \in \mathrm{C}\) \(\blacktriangleleft\) O

2 関係に関する定理

関係そのものの性質も word で書けます。関係は \(\) で引用して渡します。
\(\mathbb{W}_{++}\)([ss,p],p)R … \(:\mathsf{R}\)  \(:\mathsf{T}\)  \(:\mathsf{X}\)
\({ \mathbin{p} } :\mathsf{R}\) は反射律 \(\forall x \, x \mathbin{p} x\) 、 \({ \mathbin{p} } :\mathsf{T}\) は推移律、 \({ \mathbin{p} } :\mathsf{X}\) は対称律です。
関係そのものは \(\mathbin{\mathrm{p}}\) のような ..v^-Form で書きます(この類は紹介されません)。
同値関係のとき「関係すること」は「クラスが等しいこと」で言い換えられます。
\(( { \mathbin{\mathrm{p}} } :\mathsf{R} , { \mathbin{\mathrm{p}} } :\mathsf{T} , { \mathbin{\mathrm{p}} } :\mathsf{X} ) \Longrightarrow ( a \mathbin{\mathrm{p}} b \Longleftrightarrow \{ x \mid x \mathbin{\mathrm{p}} a \} = \{ x \mid x \mathbin{\mathrm{p}} b \} )\) \(\blacktriangleleft\) O

順序のような関係でも、クラスにすると言えることがあります。
\(\mathbb{W}_+\)(cc,p) … \(\subset\)
次は「大きいクラスほど上界は少ない」(反変)です。
\(A \subset B \Longrightarrow \{ x \mid \forall y \, ( y \in B \Longrightarrow y \mathbin{\mathrm{p}} x ) \} \subset \{ x \mid \forall y \, ( y \in A \Longrightarrow y \mathbin{\mathrm{p}} x ) \}\) \(\blacktriangleleft\) O
次は「もとのクラスは、その上界たちの下界に含まれる」です。上の反変と対で、ガロア接続の入口になります。
\(A \subset \{ x \mid \forall y \, ( y \in \{ z \mid \forall u \, ( u \in A \Longrightarrow u \mathbin{\mathrm{p}} z ) \} \Longrightarrow x \mathbin{\mathrm{p}} y ) \}\) \(\blacktriangleleft\) O

写像についても書けます。
\(\mathbb{W}_+\)(cc,c) … \(\cap\)
次は「\(\mathbin{f}\) の不動点かつ \(\mathbin{g}\) の不動点なら、続けて施しても動かない」です。
\(\{ x \mid \mathbin{\mathrm{f}} x = x \} \cap \{ x \mid \mathbin{\mathrm{g}} x = x \} \subset \{ x \mid \mathbin{\mathrm{f}} ( \mathbin{\mathrm{g}} x ) = x \}\) \(\blacktriangleleft\) O