Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Products over Finite Sets: a Single Factor, Vanishing in a Field, and Signs and Monotonicity in an Ordered Ring
lemmalem:finite-products-nbg-2026bAlgebraA product over a finite set whose factors are all 1 but one equals that factor; in a field it vanishes exactly when a factor does; and in an ordered ring it is nonnegative for nonnegative factors and monotone in them.- 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-2026bCombinatoricsSet 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.- If one integer is less than another, then it is less than the other by at least one.
The Maximum and Minimum of Two Elements of an Ordered Field: Sum, Difference and Absolute Value
lemmalem:max-min-ordered-field-nbg-2026bAlgebraIn an ordered field the maximum and minimum of two elements add up to their sum and differ by the absolute value of their difference, and the absolute value of an element is the maximum of it and its negative.- 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.Positive, Nonnegative, Negative and Nonpositive Elements of an Ordered Ring
definitiondef:sign-ordered-ring-nbg-2026aAlgebraAn element x of an ordered ring is positive if 0 < x, nonnegative if 0 ≤ x, negative if x < 0, and nonpositive if x ≤ 0.Natural Numbers Read in an Ordered Field Agree with the Canonical Embedding of the Rationals
lemmalem:ordered-field-numerals-nbg-2026bAlgebraIn every ordered field, a natural number with zero read as a multiple of 1 is the image of that natural number under the canonical embedding of the rationals.Natural Numbers Read in the Integers and in the Rationals Agree with Their Embeddings
lemmalem:numeral-images-nbg-2026bAlgebraThe image of a natural number with zero as a multiple of 1 in the integers, and in the rationals, coincides with its image under the canonical embeddings.- Fixes the standard notation in commutative rings, fields and ordered fields: negatives, differences, powers, finite sums and products, natural numbers read as multiples of 1, reciprocals and quotients, the order notation, absolute values and the sign words.
- 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.Every Sequence in a Totally Ordered Set Has a Monotone Subsequence
lemmalem:monotone-subsequence-nbg-2026aAnalysisEvery sequence in a totally ordered set has a nondecreasing subsequence or a strictly decreasing subsequence, and in particular a monotone subsequence.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).