Alphabeta Math

Finite Counting, Factorials and Binomial Coefficients

About this page
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 17 results · all verified · 14 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Definition

The cardinality | A| of a finite set

Theorem

A subset of a finite set is finite, with | B| ≤ | A|, and equality holds if and only if B = A

Definition

Finite sums and finite products of natural numbers, ∑_k<n aₖ and ∏_k<n aₖ in ℕ

Lemma

Laws of finite sums and products in ℕ, and ι(∑_k<n aₖ) = ∑_k<n ι(aₖ)

Lemma

A finite sum is unchanged by a permutation of its index range: ∑_k<n a_π(k) = ∑_k<n aₖ for every bijection π : n → n

Definition

The sum ∑_i ∈ S aᵢ over a finite index set, and its product form

Theorem

The sum rule: a finite disjoint union is finite with | A ∪ B| = | A| + | B| and |⋃_i ∈ I Aᵢ| = ∑_i ∈ I| Aᵢ|, and a sum over a finite index set splits along a partition

Theorem

The product rule: | A × B| = | A| | B|, and |∏_i<m Aᵢ| = ∏_i<m| Aᵢ|

Definition

Exponentiation of natural numbers, mⁿ, and its agreement with the integer power in ℝ

Theorem

The set A^B of functions B → A between finite sets is finite, with | A^B| = | A|^| B|

Corollary

lvertP(A)| = 2^| A| for finite A

Definition

The factorial n! and the falling factorial n^k̲, defined by recursion in ℕ

Theorem

The number of injections from a k-element set into an n-element set is n^k̲

Theorem

A finite set A with | A| = n has exactly n! bijections onto itself, and n! bijections onto any set of the same cardinality

Definition

The set [A]ᵏ of k-element subsets and the binomial coefficient C(n, k) := | [n]ᵏ|

Theorem

C(n, k) k! (n-k)! = n! for k ≤ n; hence C(n, k) k! = n^k̲, the quotient n!/(k!(n-k)!) is a natural number, and C(n, k) = C(n, n-k)

Theorem

Pascal's rule C(n+1, k+1) = C(n, k) + C(n, k+1), and the hockey-stick identity ∑_i ≤ nC(i, k) = C(n+1, k+1)

Theorem

A finite set with n elements has exactly C(n, 2) two-element subsets, and 2C(n, 2) = n(n-1)

Theorem

The binomial theorem in ℝ: (x+y)ⁿ = ∑_k<n+1 iotaC(n, k) xᵏ y^ n-k

Corollary

∑_k<n+1C(n, k) = 2ⁿ, and ∑_k<n+1(-1)ᵏiotaC(n, k) = 0 for n ≥ 1

Theorem

Vandermonde's identity C(m+n, k) = ∑_i<k+1C(m, i)C(n, k-i)

Definition

The multinomial coefficient C(n, k₀,…,kₘ₋₁) as the number of ordered partitions of an n-set into blocks of prescribed sizes

Theorem

The multinomial coefficient equals n!/∏_i<m kᵢ!, and (x₀+…+xₘ₋₁)ⁿ = ∑ iotaC(n, k)∏_i<m xᵢ^kᵢ in ℝ

Definition

Compositions and weak compositions of a natural number into a fixed number of parts

Theorem

For m ≥ 1 the number of weak compositions of n into m parts is C(n+m-1, m-1), and the number of compositions is C(n-1, m-1) for n ≥ 1

Remark

Conventions fixed on this page, and what counting is deliberately not done here

Sources