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.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.- For a set X and n in N_0, X^n is the set of maps from [n] to X, whose elements are n-tuples (x_1,...,x_n) with components x_k.
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].- For m and n in N_0, m divides n if n=mk for some k in N_0.
Parity: Every Natural Number with Zero Is Either Even or Odd, and Parity of Natural Numbers
lemmalem:parity-nbg-2026aAlgebraSet TheoryEvery element of N_0 is even or odd and not both, and for a natural number the witnesses can be taken in N.- An element n of N_0 is even if n=2k and odd if n=2k+1 for some k in N_0.
A Sum of Natural Numbers Exceeds Each Summand and Is Not One
lemmalem:natural-number-sums-nbg-2026aAlgebraSet TheoryFor natural numbers a and b, the sum a+b is strictly greater than a and differs from 1.- A map may be defined by two cases: given a property of the elements of a set and an expression for each case with values in a target set, there is exactly one map taking the first value where the property holds and the second elsewhere.
The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products
lemmalem:natural-number-image-ring-nbg-2026bAlgebraSet TheoryThe images of 0 and 1 in a commutative ring are its zero and unit, and the image of a sum, product, difference, power, finite sum or finite product of natural numbers with zero is the corresponding expression in the images.The Difference of Two Natural Numbers with Zero
definitiondef:natural-number-difference-nbg-2026aAlgebraSet TheoryFor natural numbers with zero m ≤ n, the difference n − m is the unique natural number with zero that added to m gives n.- Fixes the ordinary notation for sets, maps, binary operations and orders on top of the class theory NBG, with the facts that make it meaningful carried by reference.
Images of Unions, Intersections, Differences and Subclasses under a Function, and under an Injective Function
lemmalem:injective-images-nbg-2026aSet TheoryImages under a function preserve unions and inclusions and compose; under an injective function they also preserve intersections, differences and membership, and inclusion of images is equivalent to inclusion of the classes.Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products
lemmalem:cardinality-nbg-2026bSet TheoryThe interval {m,...,n} has (n+1)−m elements; only the empty set has no elements and a singleton has one; injective maps preserve the number of elements and arbitrary maps do not increase it; a proper subset has fewer elements; the numbers of elements of a union and an intersectio…- The number of elements #A of a finite set A is the unique n in the natural numbers with zero for which {1,...,n} can be mapped bijectively onto A.
Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice
lemmalem:finite-sets-nbg-2026cSet TheoryAn injection from [m] to [n] forces m ≤ n, so a finite set is listed by exactly one [n]; subsets, unions, Cartesian products, images and sets of maps of finite sets are finite, as are finite unions of finite sets; a set of natural numbers with zero is finite exactly when it is bo…- A set is finite if it can be listed bijectively as the elements of {1,...,n} for some n in the natural numbers with zero; otherwise it is infinite.
Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting
lemmalem:natural-number-intervals-nbg-2026bSet TheoryBasic facts about intervals of natural numbers: [n] consists of the natural numbers up to n, [0] is empty and [1]={1}, [n+1] adds the new element n+1 to [n], an interval splits into two consecutive disjoint intervals, adding p shifts an interval bijectively, and [m] ⊆ [n] exactly…