Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map
helperhlp:relation-preimage-membership-2026aSet TheoryMembership in the inverse of a class relation and in the preimage of a class, the preimage and the image under a map between classes, and enlarging the codomain of a map.Adding a Positive Real, Cancelling an Added Real, and Regrouping Four Summands in ℝ
helperhlp:real-sum-rules-2026aAlgebraFor real numbers: adding a positive number increases a number, adding and then subtracting y returns x, and a sum of two sums can be regrouped as (a+c)+(b+d).- The norm metric of a real normed space is the distance function given by the norm of the difference of two vectors.
Real Powers of the Absolute Value of a Measurable Function Are Measurable
lemmalem:power-functions-measurable-2026aAnalysisFor a measurable real function f and a real exponent a>0, the function x ↦ |f(x)|^a is measurable and lies in the set of measurable functions into [0,∞].- Standing notation for the spaces of p-integrable functions and their seminorms, the Lebesgue spaces Lᵖ(μ), the spaces L²(μ;ℝⁿ) of square-integrable vector-valued functions, and their versions on a closed interval, with the background results about them.
- L²(μ;ℝⁿ) is a real inner product space whose squared norm is the integral of |f|², the sum of the squared 2-seminorms of the components; under dependent choice it is complete, hence a real Hilbert space.
- L²(μ;ℝⁿ) is the set of classes of square-integrable ℝⁿ-valued functions under almost-everywhere equality, with the sum and scalar multiples of representatives and the inner product given by the integral of the dot product.
- Almost-everywhere equality is an equivalence relation on the p-integrable functions, compatible with sums and scalar multiples, and it preserves the p-seminorm and, for p = 2, the integral of a product.
Square-Integrable Vector-Valued Functions: Components, Dot Products and Almost-Everywhere Equality
lemmalem:l2-vector-functions-2026aAnalysisA function into ℝⁿ is square-integrable exactly when its components are, with the integral of |f|² the sum of the squared component seminorms; dot products of square-integrable functions are integrable; linear combinations stay square-integrable; and almost-everywhere equality is…- For a measurable function f from a measure space to ℝⁿ, |f|² is the function x ↦ ‖f(x)‖², and f is square-integrable if the integral of |f|² is finite.
Real Normed, Inner Product and Hilbert Spaces: Notation
settingset:normed-spaces-2026aAnalysisLinear AlgebraStanding notation for real vector spaces, real normed spaces with their norm metric, real inner product spaces regarded as normed spaces, and real Banach and Hilbert spaces.- Euclidean space with its componentwise operations and the dot product is a real inner product space whose induced norm is the Euclidean norm and whose norm metric is the Euclidean distance; it is a real Hilbert space.
- The norm metric of a real normed space is d(u,v) = ||u - v||, and the space is a real Banach space if it is complete for this metric.
- In a real normed space the zero vector has norm 0, d(u,v) = ||u - v|| is a metric, the reverse triangle inequality holds, limits respect sums, differences, scalar multiples and norms, and convergent sequences are Cauchy.
- An inner product is linear in its second argument as well; the induced norm expands squares of sums and differences, is a norm, satisfies the parallelogram law, and the inner product is continuous for the norm metric.
The Zero Vector, Negatives and Differences in a Vector Space
definitiondef:vector-space-negatives-2026aAnalysisLinear AlgebraNames the zero vector 0_V of a vector space, the negative -v of a vector v, and the difference u - v = u + (-v).Uniqueness of the Zero Vector and of Negatives
lemmalem:vector-space-zero-negatives-2026aAnalysisLinear AlgebraA vector space has exactly one zero vector, and each vector has exactly one negative with respect to it.Open Boxes: Emptiness, Intersections and Preimages under Concatenation
helperhlp:open-box-identities-2026aAnalysisAn open box with a side of nonpositive length is empty, the intersection of two open boxes is the open box with the componentwise larger lower and smaller upper corners, and the preimage of an open box in ℝ^{m+n} under concatenation is the product of the corresponding boxes in ℝ^…Integrals of Finite Sums of Nonnegative Functions, and Constant Multiples of a Measure
lemmalem:finite-sums-constant-multiples-2026aAnalysisThe integral of a finite sum of nonnegative measurable functions is the sum of their integrals; and a constant multiple cμ of a measure is a measure, the measure with constant density c, against which integrals are c times the integrals against μ.Precomposition Commutes with Pointwise Operations, and Sections of Functions Are Precompositions
helperhlp:precomposition-operations-2026aAnalysisComposing with a function T on the right commutes with positive and negative parts, absolute values, sums, multiples, indicators, pointwise suprema and dyadic approximations; and the sections of a function on a product are its composites with the insertion functions.