Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Number of Elements of a Disjoint Finite Union
lemmalem:disjoint-union-count-nbg-2026aCombinatoricsSet TheoryThe number of elements of a union of finitely many pairwise disjoint finite sets is the sum of their numbers of elements, and equals the number of sets times r when each has r elements.Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples
lemmalem:finite-set-counting-nbg-2026aCombinatoricsSet TheoryRemoving an element from a finite set lowers its number of elements by one, injective self-maps of finite sets are bijections, the natural numbers are infinite, the set of permutations of [n] is finite and nonempty, and two standard bijections: onto a slice of a product and onto…The Number of Integers between Two Integers
lemmalem:integer-intervals-nbg-2026aCombinatoricsSet TheoryFor integers a at most b, the integers x with a at most x at most b form a finite set with b-a+1 elements.Iterated Operations over an Interval: Extracting One Term and Reversing the Order
lemmalem:finite-sum-extraction-nbg-2026aAlgebraCombinatoricsFor an associative and commutative operation, one term can be taken out of the iterated operation over an interval, and the order of the terms can be reversed.- In a commutative ring the n-th power of a sum x+y is the sum over k from 0 to n of the binomial coefficient of n and k times x^k y^(n-k).
- The binomial coefficient of two natural numbers with zero is the value at that pair of the unique map satisfying Pascal's recursion.
Bijections between Intervals: the Gap Map and the Reversal
lemmalem:interval-bijections-nbg-2026aCombinatoricsSet TheorySkipping one value j gives a bijection from [n] onto [n+1] without j, and a maps to N+1-a gives a bijection of [N] onto itself that is its own inverse.Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry
lemmalem:binomial-coefficients-nbg-2026aCombinatoricsThere is exactly one map on pairs of natural numbers with zero satisfying Pascal's recursion with the boundary values 1 and 0, and it vanishes above the diagonal, is 1 on the diagonal and n at k=1, satisfies the factorial formula and is symmetric.Permutations of a Set and the Set of Permutations of [n]
definitiondef:permutation-nbg-2026aCombinatoricsSet TheoryA permutation of a set A is a bijection from A to A, and S_n is the set of permutations of [n].The Factorial: Recursion, Positivity and Bounds by Powers
lemmalem:factorial-nbg-2026aAnalysisCombinatoricsThe factorial satisfies 0! = 1 and (n+1)! = (n+1)·n!, is at least 1 and nondecreasing, and (n+1)! lies between 2^n and (n+1)^(n+1).- The factorial n! of n in the natural numbers with zero is the product of 1, ..., n in the natural numbers with zero, the empty product being 1.
The Maps from a Finite Set to a Nonempty Finite Set Form a Nonempty Finite Set
lemmalem:maps-between-finite-sets-finite-2026aCombinatoricsThe set of all maps from a nonempty finite set to a nonempty finite set is nonempty and finite.Finitely Supported Multi-Indices: Order, Factorial, Powers and Weighted Order
definitiondef:finitely-supported-multi-indices-2026aAnalysisCombinatoricsDefines multi-indices as finitely supported sequences of nonnegative integers, together with their order, factorial, powers of a real sequence, weighted order , the sets of multi-indices of a given order, and the unit multi-indices with th…Counting Cyclically Reduced Words: Finiteness and the Bound (2d)^k
lemmalem:nc-unitary-word-counts-2026aCombinatoricsWords of a given length form a nonempty finite set containing cyclically reduced words, and a sum over words of length k of terms bounded by M is at most M(2d)^k.Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability
lemmalem:words-finite-alphabet-basic-2026aCombinatoricsWords form a monoid under concatenation, reversal is an anti-multiplicative involution, every word has finitely many factorisations, and the set of words is countable.Words over a Finite Alphabet: the Empty Word, Concatenation and Reversal
definitiondef:words-finite-alphabet-2026bCombinatoricsDefines the words in finitely many letters, including the empty word, together with concatenation and reversal.Block Indices: Enumerating an Initial Segment of Length qN by Blocks and Positions
lemmalem:block-index-arithmetic-euclidean-2026bCombinatoricsThe numbers (k-1)q+i with k in [N] and i in [q], computed in the reals, are images of natural numbers that enumerate [qN] exactly once each, so a sum over [qN] splits into N blocks of q terms.- Let be a natural number, let be the initial segment determined by , and let be the set of permutations of , with the identity , the composition and the inverse of…
An Injective Self-Map of a Finite Set is a Bijection
lemmalem:injective-self-map-finite-set-bijective-2026aCombinatoricsSet TheoryLet be the set of natural numbers with successor map as in that definition, let , and let be the initial segment determined by . Call a map between sets injective if implies for all . The notions…Permutations of an Initial Segment Form a Group under Composition
lemmalem:permutation-group-2026aAlgebraCombinatoricsLet be a natural number, let be the initial segment determined by , that is, the set , and let be the set of permutations of , that is, the set of bijections from to . For maps let be th…