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.
The set of -element subsets and the binomial coefficient
Definition
For a finite set and put
the set of -element subsets of . Every is finite (A subset of a finite set is finite, with , and equality holds if and only if ), so the condition makes sense for every subset.
is finite. It is a subset of , which is finite by for finite , so A subset of a finite set is finite, with , and equality holds if and only if applies.
depends only on . Let be a bijection of finite sets. The direct image map carries into , because restricted to is a bijection of onto and so by the transport clause of The cardinality of a finite set; the map is its two-sided inverse, since and for a bijection . So and the two have the same cardinality.
Definition. For set
the binomial coefficient. By the previous paragraph and ,
is a count, so it is a natural number by construction. It is not defined as : that expression involves a division, hence lives in , and the assertion that its value is a natural number is a theorem, proved in for ; hence , the quotient is a natural number, and . Defining the coefficient as a count makes integrality free and leaves the closed formula something to prove.
Boundary values, read off the definition and not stipulated.
- for every , including : the subsets of of cardinality are exactly the subsets equal to (The cardinality of a finite set, clause (b)), so , a one-element set. No empty-product convention is involved.
- : if has then by clause 3 of A subset of a finite set is finite, with , and equality holds if and only if , so .
- for : a subset has by clause 2 of A subset of a finite set is finite, with , and equality holds if and only if , so is impossible and (Trichotomy of the order on ).
- : a subset of cardinality is for exactly one , since means ; so its unique element is a bijection .
- and for , both instances of the above.
Remarks
-
Notation. is standard for the set of -element subsets; it is unrelated to the notation for a set of functions, which appears on this page as well. Where confusion is possible the words are used in full.
-
Symmetry is not visible yet. is proved in for ; hence , the quotient is a natural number, and by exhibiting the complementation bijection ; from the definition alone there is no reason for the two counts to agree.
-
is a legitimate value of and of . Every boundary clause above is checked at , which is where a statement about binomial coefficients most often goes wrong in this library's index convention.
Depends on
- The cardinality $\lvert A\rvert$ of a finite set
- $\lvert\mathcal{P}(A)\rvert = 2^{\lvert A\rvert}$ for finite $A$
- A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, and equality holds if and only if $B = A$
- Injection, surjection, bijection
- Equinumerous sets, $A \approx B$ and $A \preceq B$
- The natural numbers $\mathbb{N}$ (von Neumann)
- Order on the natural numbers
- On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$
- Trichotomy of the order on $\mathbb{N}$
Used by
- (n+1) Cₙ=C(2n, n) Corollary
- ∑_k<n+1C(n, k) = 2ⁿ, and ∑_k<n+1(-1)ᵏiotaC(n, k) = 0 for n ≥ 1 Corollary
- A symmetric chain decomposition gives a second proof of Sperner's bound Corollary
- Dimension of the kth exterior power is binomial Corollary
- For an odd prime p, the p-th power map is a homomorphism on a finite group whose derived subgroup is central of exponent dividing p Corollary
- For d≥1 a family on [n] of VC dimension at most d has at most (n+1)ᵈ members Corollary
- For n≥1 the pairs of non-intersecting monotone paths (1,0)→(n+1,n) and (0,1)→(n,n+1) number C(2n, n)²-C(2n, n+1)C(2n, n-1) Corollary
- If dim V=n, then dimΛᵏV=C(n, k) Corollary
- Mₙ=∑_k∈ℕ, 2k≤ nC(n, 2k)Cₖ Corollary
- R(s,t)≤ R(s-1,t)+R(s,t-1) for s,t≥2, and R(k,k)leC(2k-2, k-1)≤2²ᵏ⁻² Corollary
- Rₙ=∑ₖ₌₀ⁿC(n+k, 2k)Cₖ Corollary
- Sperner's theorem and its equality cases: a largest antichain is a complete middle level Corollary
- The central binomial coefficient is asymptotic to 4ⁿ divided by the square root of pi n Corollary
- The number of diagonal paths from (0,a) to (n,b) is C(n, u) for the natural number u with 2u=n+b-a, and 0 when no such u exists Corollary
- Two sets of the same finite cardinality between which the bijection is not unique Counterexample
- When k<n<2k, the entire kth level is intersecting and exceeds the Erdős-Ko-Rado star bound Counterexample
- A finite family (Aᵢ)_i ∈ I of subsets of a finite set X, the intersections A_J for J ⊆ I, and the convention A_∅ = X Definition
- Edge density and the asymptotic notations O, o, Ω, and Θ for extremal functions Definition
- Intersecting uniform families of finite sets Definition
- r-uniform hypergraphs and complete balanced r-partite r-graphs K⁽ʳ⁾_s,…,s Definition
- The Bernstein polynomial Bₙ(f) on [0,1] Definition
- The Boolean lattice of subsets of a finite set and its rank levels Definition
- The Erdős-Rényi finite random graph G(n,p) Definition
- The inclusion matrix W_t,k(n) of t-sets against k-sets Definition
- The lower and upper shadows of a uniform set family Definition
- The multinomial coefficient C(n, k₀,…,kₘ₋₁) as the number of ordered partitions of an n-set into blocks of prescribed sizes Definition
- A two-by-two determinant counting non-intersecting path pairs Example
- All 8 functions 3 → 2, the 0 injections 3 → 2, and the 8 subsets of a 3-element set Example
- All k-sets through a fixed point form an intersecting family attaining the Erdős-Ko-Rado bound Example
- All subsets of [4] of size at most 2: VC dimension 2 and exactly ∑_i≤2C(4, i)=11 members Example
- Choosing a committee: C(10, 3) = 120, and the ordered count 10^3̲ = 720 Example
- Five-card hands from a 52-card deck: C(52, 5) = 2598960, and the count of hands with all cards of one suit Example
- For a finite symmetric irreflexive relation the sum of the neighbour counts is twice the number of unordered related pairs Example
- Lagrange inversion gives the Catalan coefficients of the inverse of x-x² Example
- Negative binomial series: (1-x)⁻ᵐ=∑_n≥0C(m+n-1, n)xⁿ for m≥1 Example
- Pascal's triangle computed to row 6, with Pascal's rule checked at every interior entry Example
- The 15 weak compositions of 4 into 3 parts, listed and matched against stars and bars Example
- The ballot problem with three votes for A and two for B Example
- The Catalan numbers through C₆, from the recurrence and from the closed formula Example
- The cycle lemma on the word (-1,+1,+1,-1,+1,-1,+1) Example
…and 78 more results.
Dependency tree · two levels
36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Binomial coefficient (Wikipedia) (standard reference, not scraped)
- Combination (Wikipedia) (standard reference, not scraped)
- R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1 (standard reference, not scraped)