Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Multinomial Coefficients: Binomial Products and Counting
lemmalem:multinomial-coefficients-2026aCombinatoricsA multinomial coefficient with one more entry is the previous one times a binomial coefficient, with two entries it is a binomial coefficient, and it counts the maps from [n] to [m] with prescribed fibre sizes.- There are C(n+k,k) tuples of k+1 natural numbers with sum n, and as many tuples of k+1 positive integers with sum n+k+1.
- Inclusion and exclusion gives alternating-sum formulas for the number of surjections from [n] onto [k] and for the number of permutations of [n] without fixed points.
- The number of elements of a finite set lying in none, or in at least one, of finitely many subsets is the alternating sum of the sizes of their intersections.
- The row sum, the alternating row sum, absorption, Vandermonde's identity, the hockey-stick identity and the weighted row sum for binomial coefficients.
- A set with n elements has C(n,k) subsets with k elements and 2^n subsets in all, and a sum over its subsets of a function of their size can be grouped by size.
- Fixes the notation of finite combinatorics on the routine-facts background: numbers of elements, sets of maps and subsets, factorials, binomial, falling-factorial and multinomial coefficients, and the reading of signed identities in the reals.
- The falling factorial satisfies (n)_n = n! and (n)_k = k! C(n,k); it vanishes for k > n and is positive for k ≤ n.
- The multinomial coefficient of a tuple of natural numbers with zero is the unique natural number that, multiplied by the product of the factorials of the entries, gives the factorial of their sum.
- The falling factorial (n)_k is the value at (n,k) of the unique map satisfying the falling-factorial recursion.
Existence and Uniqueness of the Multinomial Coefficients
lemmalem:multinomial-coefficient-existence-2026aCombinatoricsFor a tuple of natural numbers with zero, the product of the factorials of its entries divides the factorial of their sum, with exactly one quotient in N_0.- Between finite sets with k and n elements there are n^k maps and (n)_k injections, n! bijections when k = n and none otherwise, and there are n! permutations of [n].
Existence and Uniqueness of the Falling Factorials
lemmalem:falling-factorial-recursion-2026aCombinatoricsThere is exactly one map F on pairs of natural numbers with zero with F(n,0)=1, F(0,k+1)=0 and F(n+1,k+1)=(n+1)F(n,k).The Sets of Injections, Surjections and Bijections between Two Sets
definitiondef:map-sets-2026aCombinatoricsFor sets A and B, Inj(A,B), Surj(A,B) and Bij(A,B) are the subsets of B^A consisting of the injective, surjective and bijective maps from A to B.- For a set A and k in N_0, P_k(A) is the set of finite subsets of A with exactly k elements.
Counting by Fibres, Double Counting and the Pigeonhole Principle
lemmalem:fibre-counting-2026aCombinatoricsA finite set is counted by summing the sizes of the fibres of a map on it; consequences are double counting of a relation, the pigeonhole principle and the count for maps with fibres of equal size.- Powers of natural numbers with zero are natural numbers with zero, satisfy the recursion and the laws for sums of exponents and products of bases, are 1 for base 1 and 0 for base 0 with positive exponent, and are at least 1 for a base at least 1.
Reading Natural Numbers in ℝ: Injectivity, Order and Pascal's Rule
helperhlp:natural-numbers-in-reals-2026aSet TheoryReading natural numbers with zero as real numbers is injective and preserves and reflects the order, and Pascal's rule holds in ℝ.- The number of elements is given by a predicative formula, so counting the members of a family of finite sets, or the subsets of a finite set, defines a map into the natural numbers with zero.
Counting through Bijections, Injections and Surjections
lemmalem:counting-through-maps-2026aCombinatoricsSet TheoryA bijection preserves finiteness and the number of elements; an injection into a finite set, and a surjection from a finite set, bound the number of elements from the appropriate side.