順序と区間・部分集合の個数・値ごとに分けて数える道具（Mathlib の card_eq_sum_card_fiberwise にあたる LΣg）・組合せの数。

1 順序と区間

word(ss,p) … \(\le\)  \(<\)
≤. … \(m \le n \Longleftrightarrow \exists k \in \mathbb{M} . m + k = n\)
<. … \(m < n \Longleftrightarrow m + 1 \le n\)
word(ss,s) … \(\mathinner{\ldotp\ldotp}\)
... … \(m \mathinner{\ldotp\ldotp} n = \{ i \in \mathbb{M} \mid m \le i \le n \}\)
L+c … \(x , y , k \in \mathbb{M} , x + k = y + k \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，Ax1 ，Ax+
\(0\) 以上の自然数。\(0 .. (m+1)\) は \(0 .. m\) に \(m+1\) を足したもの。
\(m\) 個の集合の部分集合の個数は \(0 .. m\) のどれか。
Lsz … \(X \stackrel{\#}= m \in \mathbb{M} \Longrightarrow \forall A \subset X . \exists k \in 0 \mathinner{\ldotp\ldotp} m . A \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，Ax1 ，Ax+

2 値ごとに分けて数える

\(S\) の各元に \(Y\) の元 \(a\) が1つずつ対応し（\(R\)）、\(a\) に対応する元がちょうど \(g(a)\) 個なら、\(S\) は \(\{(a, j) \mid a \in Y, j \in g(a)\}\) と個数が等しい（Mathlib の card_eq_sum_card_fiberwise）。\(a\) を1つ除いた場合から帰納法で示す。
どの値の部分もちょうど \(q\) 個なら、\(S\) は \(q \cdot k\) 個（\(Y\) は \(k\) 個）。

3 組合せの数

\(n \mathrm{C} k\) は \(n\) 個の集合の \(k\) 元部分集合の個数（AxC）。choose=# は \(n\) 個の集合 \(X\) でも同じ個数であること。
word(ss,s) … \(\mathrm{C}\)
AxC … \(n , k \in \mathbb{M} \Longrightarrow n \mathrm{C} k \in \mathbb{M} , n \mathrm{C} k \stackrel{\#}= \{ A \in \wp n \mid A \stackrel{\#}= k \}\)
word(ss,s) … *^ap
*^ap. … \(R ( A ) = \{ y \mid \exists x \in A . \langle x , y \rangle \in R \}\)
0 元部分集合は空集合だけ。