Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- A sequence of real numbers is bounded above or below when the set of its terms is, and bounded when the absolute values of its terms have a common bound.
- A sequence in a partially ordered set is nondecreasing, strictly increasing, nonincreasing or strictly decreasing when each term compares accordingly with the next, and monotone when it is nondecreasing or nonincreasing.
- A sequence in a set X is a map from the natural numbers to X; its value at n is its n-th term.
Arbitrary Positive Slack, and Approximation of Suprema and Infima, in the Real Numbers
lemmalem:real-approximation-nbg-2026bAnalysisAlgebraIn the real numbers, an inequality that holds up to every positive slack holds exactly, a nonnegative number below every positive number is zero, and the supremum or infimum of a nonempty set bounded above or below is approached by elements of the set, strictly and within every p…Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares
lemmalem:ordered-field-inequalities-nbg-2026cAlgebraFurther rules of order in an ordered field: mixed transitivity, adding a strict and a weak inequality, strict sign reversal, positivity of products, positivity of the natural numbers, halving, order of reciprocals, the strict absolute-value bound, the reverse triangle inequality,…Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field
lemmalem:commutative-ring-rules-nbg-2026cAlgebraIn a commutative ring, multiplying by zero gives zero, the sign rules hold, squares of sums and differences expand and differences of squares factor; a field has no zero divisors.The Image of a Natural Number in a Commutative Ring
definitiondef:natural-number-image-ring-nbg-2026bAlgebraThe image of a natural number n in a commutative ring is the sum of n copies of the unit, and the image of 0 is 0.- If e and e' are neutral elements of the same binary operation, then e = e*e' = e'.
Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality
lemmalem:finite-set-sums-nbg-2026dAlgebraSums over finite sets in a commutative ring distribute over multiplication, commute with differences, multiply as a sum over the product set, ignore vanishing terms, give the number of elements times a constant term, can be taken over dependent pairs, and a product of sums expand…Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals
lemmalem:finite-set-operation-properties-nbg-2026bAlgebraFor an associative and commutative operation with a neutral element, the iterated operation over finite sets is additive over disjoint unions, invariant under reindexing by a bijection, computed over a product of sets as an iterated double operation in either order, combines term…Sums and Products over a Finite Set and over an Interval
definitiondef:finite-set-operation-nbg-2026bAlgebraFor an associative and commutative operation, the iterated operation of a map over a nonempty finite set is taken along any enumeration of the set, over the empty set it is the neutral element, and over an interval {m,...,n} it gives the sums and products from k=m to n.The Iterated Operation over a Finite Set Does Not Depend on the Enumeration
lemmalem:finite-set-operation-nbg-2026bAlgebraFor an associative and commutative operation, iterating it over the values of a map on a nonempty finite set gives the same result for every enumeration of the set.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.
Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality
lemmalem:natural-powers-nbg-2026dAlgebraPowers satisfy the exponent laws and the factorisation of x^n - y^n; in a field the powers of a nonzero element are nonzero and the geometric sum formula holds; in an ordered field powers of nonnegative elements are nonnegative and strictly increasing in the base, monotone in the…Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality
lemmalem:finite-sums-nbg-2026cAlgebraFinite sums in a commutative ring distribute over multiplication, commute with negatives and differences, telescope, and a sum of n equal terms is n times the term; in an ordered field sums preserve (strict) inequalities between terms, a sum of nonnegative terms dominates each te…Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms
lemmalem:iterated-operation-properties-nbg-2026bAlgebraAn iterated operation obeys its recursion; for an associative operation it splits into the iterated operations of two consecutive blocks; for an associative and commutative operation it is unchanged by reordering the terms and combines termwise; and maps preserving the operation…- For an element x of a set with a multiplication, x^n is the product of n copies of x, and x^0 is the neutral element when there is one.