Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Existence and Uniqueness of Nonnegative k-th Roots of Nonnegative Real Numbers
lemmalem:roots-nbg-2026aAnalysisFor 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-2026bAnalysisNonempty 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-2026bAnalysisIn 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-2026bAnalysisA 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.
- 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-2026aAnalysisAlgebraIn 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…The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness
settingset:real-numbers-nbg-2026cAnalysisAlgebraFixes the real numbers as an ordered field with the standard notation, identifies natural numbers, integers, rationals and sets of them with their images in the reals, so that N ⊆ N_0 ⊆ Z ⊆ Q ⊆ R, and carries completeness with its consequences: infima, the Archimedean property, d…Ordered Fields in Which Every Nonempty Set Bounded Above Has a Supremum Are Unique up to Unique Isomorphism
theoremthm:least-upper-bound-ordered-field-unique-nbg-2026bAnalysisAlgebraFor any two ordered fields in which every nonempty set bounded above has a supremum, there is exactly one homomorphism of ordered fields from the first to the second; it is an isomorphism and it fixes every rational number.The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum
theoremthm:real-numbers-nbg-2026aAnalysisAlgebraThe real numbers form an ordered field in which every nonempty set bounded above has a supremum, and the canonical embedding of the rationals sends each rational to its rational cut.Infima, the Archimedean Property, Density of the Rationals and Rational Approximation from Below in an Ordered Field Whose Nonempty Sets Bounded Above Have Suprema
lemmalem:least-upper-bound-ordered-field-nbg-2026bAnalysisAlgebraIn an ordered field in which every nonempty set bounded above has a supremum, nonempty sets bounded below have infima, every element lies below some natural number, the rationals are dense, and every element is the supremum of the rationals below it.Compatible Noise Penalty Pairs at a Fine and a Coarse Level
definitiondef:compatible-noise-penalty-pairs-hilbert-2026aAnalysisProbabilityTwo noise penalty pairs at a fine and a coarse level, joined by a mode-restriction link, are compatible with constant c_0 if the push-forward under the mode restriction maps the fine penalty and score domains into the coarse ones and raises the penalty by at most c_0.Two Noise Levels over Hilbert Spaces: a Fine and a Coarse Reading of the Noise Framework and Level-Indexed Notation
settingset:noise-levels-hilbert-2026aAnalysisProbabilityFixes two readings, a fine and a coarse level, of the standing noise Wasserstein and noise penalty framework over two Hilbert spaces with their bases, noise weights and reference measures, together with the level-indexed notation (noise norms, field norms, couplings, distances, t…