Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Sections of a Sequence of Maps into a Metric Space, and the Map of Their Limits
helperhlp:sections-limit-maps-metric-2026aAnalysisFor a sequence of maps from a set D into a metric space, each evaluation at a point of D is a sequence in the space, and if these sections converge at every point of a subset S of D there is exactly one map on S to which they converge pointwise, its value at each point being the…Maps Given by Integrals of Vector- and Matrix-Valued Maps
helperhlp:vector-matrix-integral-maps-2026aAnalysisFor a vector- or matrix-valued map on a subset E of the reals whose integral from c to t is defined for every t in a subset S of E, there is exactly one map on S whose value at each t is that integral.The Distance Between the Values of Two Continuous Maps Is Continuous
lemmalem:distance-continuous-maps-2026aAnalysisTopologyFor continuous maps x and y from a subset A of a metric space into a metric space Y, the real-valued map t ↦ d_Y(x(t), y(t)) is continuous on A.Radial Retraction onto a Closed Ball in ℝⁿ and in the Real Matrices
lemmalem:radial-retraction-ball-2026aAnalysisFor R > 0, the radial retraction that fixes the points of norm at most R and rescales the others to norm R is a well-defined map into the closed ball of radius R and is Lipschitz with constant 2, both on Euclidean space with the Euclidean norm and on real matrices with the operat…The Diagonal Sets of the Cauchy Product and Re-indexing of Diagonal Sums
helperhlp:cauchy-product-diagonal-2026aCombinatoricsDescribes the elements of the diagonal set D_n of pairs (i,j) in [n]x[n] with i+j=n+1, shows it is a finite set of pairs of natural numbers, and re-indexes a sum over D_{m+1} as a sum from k=0 to m via the bijection k -> (k+1,(m-k)+1).Solutions of an Initial Value Problem Are the Continuous Solutions of the Integral Equation
lemmalem:initial-value-problem-integral-form-2026aAnalysisFor a continuous right-hand side F, a map x on [a,c] solves x' = F(t,x), x(a) = xi, exactly when it is continuous and x(t) = xi + integral from a to t of F(s,x(s)); along a continuous x the integrand is continuous.The Weighted Uniform Distance Is a Metric, and Is Complete When the Target Is Complete
lemmalem:weighted-uniform-distance-complete-2026aAnalysisTopologyFor a continuous positive weight w on [a,b] and a metric space Y, the weighted uniform distance d_w is a metric on C([a,b],Y); C([a,b],Y) is nonempty when Y is, and complete when Y is complete.The Space of Continuous Maps on a Closed Interval and Its Weighted Uniform Distance
definitiondef:weighted-uniform-distance-2026aAnalysisTopologyDefines the set C([a,b],Y) of continuous maps from a closed interval into a metric space and, for a continuous positive weight w, the weighted uniform distance d_w(x,y), the maximum over t of w(t) d_Y(x(t),y(t)).- A solution on [a,c] of the initial value problem x' = F(t,x), x(a) = xi, is a differentiable map on [a,c] satisfying the equation at every point and the initial condition; a solution on [a,b] is called a solution.
The Initial Value Problem for a First-Order System of Ordinary Differential Equations
equationeq:initial-value-problem-2026aAnalysisThe system x'(t) = F(t, x(t)), x(a) = xi, for an unknown map x from an interval [a,c] into R^n, and the same system for matrix-valued unknowns.Rules for Oriented Riemann Integrals of Real-Valued Maps: Sums, Scalar Multiples, Constants, Continuous Maps, Additivity and Evaluation by an Antiderivative
lemmalem:oriented-integral-rules-2026aAnalysisOriented Riemann integrals of real-valued maps are linear and integrate constants, are defined for continuous maps on an interval and additive over any three points there, and integrate a derivative to the difference of the values of the map.Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps
helperhlp:pointwise-maps-2026aSet TheoryFor sets S, Y, Z, W and J, the constant maps from S into Y, the pairing u ↦ (f(u), g(u)) of two maps on S, the maps u ↦ F(f(u), g(u)) and u ↦ Φ(f(u)), and the family of maps u ↦ G(j, u) indexed by j in J exist and are unique.- Names the k-th component map of a map into R^q and the (i,j) entry map of a map into p-by-q real matrices, as the real-valued maps taking the corresponding component or entry of each value.
A Predicative Formula for Continuity at a Point, and the Set of Real-Valued Maps Continuous at a Point
helperhlp:continuity-predicative-2026aSet TheoryUnder the guard that g is a map from a subset S of a metric space into a metric space and s is a point of S, continuity of g at s relative to S is expressed by a predicative formula; consequently the real-valued maps on S continuous at a given point of S form a set, a subset of t…Component Maps of a Map into , Entry Maps of a Map into Matrices, and Maps Assembled from Them
helperhlp:component-entry-maps-2026aAnalysisA map from a set S into R^q has one real-valued component map for each index, and a map into the real p x q matrices one real-valued entry map for each pair of indices, each family forming a map into the set of real-valued maps on S; conversely, every such family of real-valued m…Finite Sums of Real-Valued Maps: Continuity, Integral and Derivative
lemmalem:finite-sum-maps-calculus-2026aAnalysisA finite sum of real-valued maps indexed by a finite set is continuous at a point, integrable between two points, or differentiable at a point whenever each summand is, with the integral and the derivative of the sum being the corresponding sums.The Fundamental Theorem of Calculus and the Mean Value Inequality for Vector- and Matrix-Valued Maps
lemmalem:vector-matrix-ftc-2026aAnalysisFor vector- and matrix-valued maps on an interval, the indefinite integral of a continuous map is an antiderivative, an integral of a derivative is the difference of endpoint values, a map with zero derivative is constant, and a bound M on the norm of the derivative gives the Lip…Rules for Derivatives of Vector- and Matrix-Valued Maps
lemmalem:vector-matrix-derivative-rules-2026aAnalysisDifferentiable vector- and matrix-valued maps on an interval are continuous, and their derivatives obey the sum, scalar, product, matrix-vector, dot-product, transpose, constant and chain rules.Rules for the Riemann Integral of Vector- and Matrix-Valued Maps
lemmalem:vector-matrix-integral-rules-2026aAnalysisContinuous vector- and matrix-valued maps on an interval are integrable, and their integrals are additive, linear, compatible with constant factors and transposes, take the value (v-u)c on a constant c, and are bounded in norm by the integral of the norm.Continuity of Vector- and Matrix-Valued Maps: the Componentwise Criterion, Norms and Algebraic Operations
lemmalem:componentwise-continuity-2026aAnalysisLinear AlgebraA map from a subset of a metric space into Euclidean space or into real matrices is continuous at a point exactly when each component or entry is; norms, constants, sums, scalar multiples, dot products, matrix products, matrix-vector products and transposes of such maps continuou…