Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Standing notation for higher derivatives on open subsets of ℝⁿ: it extends the multivariable calculus notation and fixes the first-order notions (partial derivatives, Jacobian matrix, gradient, differentiability) with their background results.
The Derivative of a Vector-Valued Function as a Limit of Difference Quotients in Norm
lemmalem:vector-derivative-norm-quotient-2026aAnalysisMultivariable CalculusA vector-valued function on an interval is differentiable at a point with a given derivative exactly when its difference quotients converge to that vector in the Euclidean norm.The Mean Value Theorem and Inequality on Convex Open Sets
lemmalem:mean-value-inequality-euclidean-2026aOn a convex open subset of R^n, a differentiable real-valued function satisfies the mean value theorem along segments, a differentiable function whose derivative matrices are bounded in operator norm by M is M-Lipschitz, and a function with vanishing derivative is constant.- Constant and affine functions and the coordinate functions are differentiable with the expected derivative matrices and gradients, and differentiability at a point is preserved by sums, scalar multiples, products and quotients, with the usual formulas.
- A function on an open subset of R^n that is differentiable at a point is continuous there; quantitatively, near the point its increments are bounded by the operator norm of the derivative matrix (or the norm of the gradient) plus one, times the length of the step.
Multivariable Calculus: Notation
settingset:multivariable-calculus-notation-2026aMultivariable CalculusStanding notation for first derivatives of functions on open subsets of R^n: dimensions, the open domain, component functions, standard basis vectors, open balls and the metrics for continuity.Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity
settingset:routine-toolkit-2026hSet TheoryExtends the routine-facts setting by the bookkeeping helpers for typed arithmetic, maps, the order of the natural numbers and predicativity, so that settings adopting it use them without citation.Maps from Functional Predicative Relations, and Families of Sections
helperhlp:functional-relation-maps-2026aA predicative formula in two set variables defines a relation, a map when it is functional on a class, and every class relation R gives the map u to the set of w in b with (u,w) in R.Events of a Probability Space: Subsets of Ω, Real Probabilities, Complements and Tail Unions
helperhlp:probability-events-2026aEvents are subsets of Ω with real probabilities between 0 and 1 in the type Real, complements have probability 1 − P(E), and the tail unions and the limsup of a sequence of events are events, the tail unions forming a decreasing sequence in the σ-algebra.- Defines the type Natural of natural numbers with zero, with the operations, order and numerals of the natural numbers with zero, under which it is a commutative semiring with cancellation and a linearly ordered additive structure.
- Addition and multiplication of the natural numbers with zero, and of any commutative ring, are associative and commutative binary operations with neutral elements 0 and 1.
- The order, successor, addition, cancellation and multiplication laws of the natural numbers with zero, the natural numbers as the numbers j+1, and basic facts on the segments [n], each as a separate flat statement.
Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages
helperhlp:map-bookkeeping-2026aBookkeeping facts for maps between classes: values and pairs of a map, equality by values, restrictions, constant maps, pairs in a product, and membership in preimages and in preimages of intersections.Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions
helperhlp:combinatorics-predicative-atoms-2026aConditions such as finiteness, number of elements, segments, intervals, tuples, maps and bijections from a segment, iterated operations, powers, binomial and multinomial coefficients, images and complements are predicative at any variable positions.- A predicative formula stays predicative, with the expected reading, when its variables are renamed or extended, when variables or set-valued parameters are substituted for them, and, under a guard, when typed terms are substituted; and its truth depends only on the sets assigned…
- A derangement of [n] is a permutation of [n] that fixes no point, and D_n is the set of derangements of [n].
- A map on C ∪ {x}, with x not in C, is the same as a map on C together with a value at x; and the injections into D taking the value b at x correspond, by restriction, to the injections from C into D without b.
A Natural Number with Zero Is Less Than Its Sum with a Natural Number
lemmalem:natural-less-than-sum-2026aSet TheoryAdding a natural number to a natural number with zero makes it strictly larger.Gluing Maps on Disjoint Domains, and Shrinking the Codomain
lemmalem:gluing-maps-2026aCombinatoricsSet TheoryTwo maps on disjoint domains glue to a map on the union, and two bijections with disjoint domains and disjoint codomains glue to a bijection; a map may be regarded as a map into any class containing its image, and an injective map is a bijection onto its image.The Multinomial Theorem in a Commutative Ring
theoremthm:multinomial-theorem-2026aAlgebraCombinatoricsThe n-th power of a sum of m elements of a commutative ring is the sum, over all exponent tuples with sum n, of the multinomial coefficient times the corresponding monomial.