Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
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).- 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.
- In a totally ordered set, any two elements a and b have a maximum and a minimum, which are the larger and the smaller of the two, and they are the least upper and greatest lower bounds of a and b.
Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits
lemmalem:root-properties-nbg-2026bAnalysisThe k-th root inverts the k-th power on nonnegative reals, the square root of a square is the absolute value, roots are multiplicative, strictly increasing and subadditive, the difference of roots is at most the root of the difference, and roots of a convergent nonnegative sequen…- The k-th root of a nonnegative real number x is the unique nonnegative real number whose k-th power is x; the second root is the square root.
Existence and Uniqueness of Nonnegative k-th Roots of Nonnegative Real Numbers
lemmalem:roots-nbg-2026bAnalysisFor every natural number k and every nonnegative real number x there is exactly one nonnegative real number whose k-th power is x.- The integer part of a real number x is the unique integer n with n ≤ x < n+1.
The Integers in the Real Numbers: Greatest Elements, the Integer Part, and Archimedean Consequences
lemmalem:integer-part-nbg-2026cAnalysisNonempty sets of integers bounded above by a real number have a greatest element, every real number lies in exactly one interval from an integer n to n+1, and the Archimedean property gives multiples of any positive number above any real number, 1/n between 0 and any positive num…Completeness of the Real Numbers for Sequences: Monotone Convergence, the Bolzano-Weierstrass Theorem and Cauchy Sequences
theoremthm:real-sequences-complete-nbg-2026cAnalysisIn the real numbers, 1/n and r^n for |r| < 1 tend to 0, a monotone bounded sequence converges to the supremum or infimum of its terms, every bounded sequence has a convergent subsequence, and a sequence converges exactly when it is a Cauchy sequence.- A sequence of real numbers is a Cauchy sequence if for every ε > 0 any two terms from some index on are within ε of each other.
- The limit of a convergent sequence of real numbers is the unique real number to which it converges.
Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences
lemmalem:limits-nbg-2026cAnalysisA sequence of real numbers converges to at most one limit; convergent sequences are bounded, and boundedness means bounded above and below; convergence ignores finitely many terms and index shifts; limits respect sums, multiples, negatives, differences, products, quotients, absol…- A sequence of real numbers converges to L if for every ε > 0 all terms from some index on lie within ε of L; it is convergent if it converges to some real number, and a null sequence if it converges to 0.
Monotone Sequences and Subsequences: Comparison of All Terms, Growth of the Indices, and Subsequences of Subsequences
lemmalem:sequences-nbg-2026bAnalysisA monotone sequence compares any two of its terms in the order of their indices; a strictly increasing sequence of natural numbers satisfies σ(k) ≥ k and preserves and reflects order; and a subsequence of a subsequence is a subsequence.- A subsequence of a sequence (a_n) is the sequence (a_{σ(k)}) obtained by composing with a strictly increasing sequence σ of natural numbers.