Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Iterated Operations: Finite Sums and Finite Products
definitiondef:iterated-operation-nbg-2026cAlgebraThe iterated operation of a list a_1,...,a_n combines its terms from left to right; written additively it is the finite sum, written multiplicatively the finite product.- For a binary operation on a set and a list a_1,...,a_n of its elements, there is exactly one list of partial results s_1,...,s_n with s_1=a_1 and s_{k+1}=s_k * a_{k+1}.
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…- For natural numbers with zero m and n, the interval {m,...,n} consists of the k with m ≤ k ≤ n, and [n] denotes {1,...,n}.
Associative and Commutative Binary Operations, and Neutral Elements
definitiondef:operation-laws-nbg-2026bAlgebraA binary operation is associative if regrouping does not change a product of three elements, commutative if the order of two factors does not matter, and an element is neutral if combining it with any element returns that element.The Natural Numbers with Zero and Their Embedding into the Integers
lemmalem:natural-numbers-with-zero-nbg-2026bAlgebraSet TheoryThe set of natural numbers with zero is the set of natural numbers together with zero, and sending zero to the integer zero and each natural number n to the integer ι(n) gives an injective map into the integers that preserves sums, products and order, with the nonnegative integer…The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness
settingset:real-numbers-nbg-2026dAnalysisAlgebraFixes 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-2026cAnalysisAlgebraFor 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-2026bAnalysisAlgebraThe 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.Multiplication of Dedekind Cuts: Associativity, Commutativity, Unit, Distributivity, Reciprocals and Nonnegative Products
lemmalem:dedekind-cut-multiplication-nbg-2026bAlgebraSet TheoryMultiplication of Dedekind cuts is associative, commutative and distributive over addition, has the cut of 1 as unit, gives every nonzero cut a reciprocal, keeps products of nonnegative cuts nonnegative, and multiplies rational cuts like the rationals.Addition and Order of Dedekind Cuts: an Ordered Abelian Group in Which Every Nonempty Set Bounded Above Has a Supremum
lemmalem:dedekind-cut-addition-order-nbg-2026bAlgebraSet TheoryAddition of Dedekind cuts is associative and commutative with neutral element the zero cut and inverses given by the negative; it respects inclusion; every nonempty set of cuts bounded above has its union as supremum; and rational cuts add and compare like the rationals.- The real numbers are the Dedekind cuts of the rationals, ordered by inclusion, added elementwise, and multiplied through the products of their absolute values with the sign fixed by the signs of the factors; zero and one are the cuts of the rationals 0 and 1.
Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts
lemmalem:dedekind-cut-construction-nbg-2026bAlgebraSet TheoryThe downward-closed proper nonempty sets of rationals without a greatest element form a set, totally ordered by inclusion; rational cuts, sums, negatives and products of nonnegative cuts are again such sets.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-2026cAnalysisAlgebraIn 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.The Canonical Embedding of the Rational Numbers into an Ordered Field
definitiondef:ordered-field-rational-embedding-nbg-2026bAlgebraThe canonical embedding of the rationals into an ordered field is the unique map from the rationals preserving sums, products and the unit.The Rational Numbers Embed in Exactly One Way into Every Ordered Field
lemmalem:ordered-field-rational-embedding-nbg-2026bAlgebraIn every ordered field there is exactly one map from the rationals preserving sums, products and the unit; it is an injective homomorphism of ordered fields that preserves and reflects the strict order, negatives and reciprocals.Homomorphisms and Isomorphisms of Ordered Fields
definitiondef:ordered-field-homomorphism-nbg-2026bAlgebraA homomorphism of ordered fields is a map preserving sums, products, the unit and the order; an isomorphism is a bijective homomorphism that also reflects the order.The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals
settingset:rational-numbers-nbg-2026dAlgebraSet TheoryFixes the integers as an ordered ring and the rationals as an ordered field, with the standard notation, and identifies natural numbers, integers and sets of them with their images in the rationals, so that N ⊆ N_0 ⊆ Z ⊆ Q.The Natural Numbers and the Integers inside the Rational Numbers
lemmalem:rational-embedding-nbg-2026bAlgebraSet TheoryInside the rationals, the natural numbers sit via n ↦ j(ι(n)), which is injective, positive and preserves 1, sums, products and order; the negations of Z and Q are their ring negatives; and every rational [x, m] is the quotient of the integer x by the natural number m.Rules of Arithmetic and Order in an Ordered Field
lemmalem:ordered-field-rules-nbg-2026bAlgebraSet TheoryThe familiar rules in an ordered field: zero products, signs, reciprocals, adding and multiplying inequalities, squares are nonnegative and 0 < 1, reciprocals of positive elements, the midpoint of two elements lies strictly between them, and the properties of absolute value inclu…