Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Bounded Linear Functionals and the Dual Space of a Real Normed Space
definitiondef:dual-space-2026aAnalysisA bound for a linear functional F on a real normed space is a real C with |F(x)| ≤ C‖x‖ for all x; the dual space is the set of linear functionals that have a bound.- A real-valued function on a linear subspace of a real vector space is a linear functional if it is additive and commutes with real multiples.
- A subset of a real vector space is a linear subspace if it contains the zero vector and is closed under sums and real multiples.
Separable Real Normed Spaces and Hahn–Banach: Notation
settingset:separable-normed-notation-2026aAnalysisStanding notation for the choice-free Hahn–Banach and separation theorems in separable real normed spaces: balls and compact sets of a normed space, countable sets, and approximation of suprema and infima.- For a nonzero element x of the type Real, the reciprocal x⁻¹ is the element whose set is the reciprocal of x in ℝ; it satisfies x·x⁻¹ = 1, x⁻¹ ≠ 0 and (x⁻¹)⁻¹ = x, and 0 ≠ 1.
- Restricting a class of sets to A and then to a subclass B of A is restricting it to B, and likewise for the restriction of a measure.
Upper Bounds of Elements of [0,∞], and the Graph of a Section of a Map on ℕ×X
helperhlp:extended-nonnegative-bounds-sections-2026aAnalysisA least upper bound in [−∞,∞] of a class containing an element of [0,∞] lies in [0,∞]; and a map g on X that agrees with the section w(n,·) of a map w on ℕ×X has its graph pairs (y,v) carried to pairs ((n,y),v) of w.- Elements of [0,∞]×[0,∞] satisfying a condition on their components are exactly the ordered pairs of elements of [0,∞] satisfying it; and the real sum and the real product of two nonnegative real numbers lie in [0,∞].
Measurable-Space Bookkeeping: Borel σ-Algebras of Metric Spaces, Closed Subintervals in the Restricted Borel σ-Algebra, and the Whole Space Almost Everywhere
helperhlp:measurable-space-bookkeeping-2026aAnalysisProbabilityThe Borel σ-algebra of a metric space is a σ-algebra, a closed interval inside [a,b] belongs to the Borel σ-algebra of ℝ restricted to [a,b], and the whole space of a measure space holds almost everywhere.- For every natural number n, the image ι(n) under the embedding of the natural numbers into the integers is an integer.
- For a positive exponent, the real power is nondecreasing in its base on the nonnegative reals.
The Origin of ℝⁿ Has Dot Product Zero with Every Point
lemmalem:origin-dot-zero-rn-2026aAnalysisLinear AlgebraMultivariable CalculusThe dot product of the origin of ℝⁿ with any point of ℝⁿ is zero.- In ℝ, 1 ≤ 1+1, and a difference x − y equal to 0 forces x = y.
- The maps τ_m used to define multiplication on ℕ₀ are maps ℕ₀×ℕ₀→ℕ₀ with τ_m((k,v))=v+m; the product m·n is the value at n of the unique recursion map, characterized both through values and through membership of pairs; membership in the multiplication class is described; and the c…
Further Order Facts for ℕ₀ in Flat Form: ≤ as Membership or Equality, Transitivity for Sets, and the Order against +1
helperhlp:omega-order-successor-2026aOn ω, m ≤ n means m ∈ n or m = n; the order is transitive for arbitrary sets; adding 1 preserves and reflects the order; m < n exactly when m+1 ≤ n; and 1 lies below every successor and every nonzero element.Values of Variables and Set Parameters Are Sets; a Predicative Monotonicity Condition
helperhlp:term-values-monotone-condition-2026aUnder every assignment of sets to x_0,...,x_{n-1}, a variable x_j with j<n and a parameter whose value is a set have sets as values; and the condition on x_0 that for every natural number m with m ≤ x_0 there are sets a and b with (m,a) and (x_0,b) in a class F and a ≤ b in the e…Class Comprehension in Two and Three Set Variables, Stated with Ordered Pairs
helperhlp:pair-triple-comprehension-2026aInstances n = 2 and n = 3 of the class comprehension theorem, written with the ordered pair (u,v) and the nested pair ((u,v),w) instead of tuples.- Intervals of natural numbers with zero are sets, and a class containing A ∪ {b} contains A and b.
Integrable and Square-Integrable Vector-Valued Functions Are Maps into
helperhlp:vector-function-spaces-maps-2026aEvery element of L^1(mu; R^n) or of L^2(mu; R^n) on a measure space, and every element of L^2(P; R^n) on a probability space, is a map from the underlying set into R^n.- A point x of R^n, being a map from [n] to R, contains the ordered pair (k, v) for k in [n] exactly when v is the k-th component of x.