Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- The convex hull of a subset S of R^n is the smallest convex subset of R^n containing S.
Existence and Uniqueness of the Smallest Convex Superset of a Subset of
lemmalem:convex-hull-existence-rn-2026aAnalysisEvery subset S of R^n has exactly one convex superset contained in every convex superset of S, namely the intersection of all convex supersets of S.- The gauge of an open convex set U containing 0 is a sublinear functional, lies between 0 and ‖x‖/r when the ball of radius r about 0 lies in U, and U is exactly the set where the gauge is less than 1.
The Minkowski Gauge of an Open Convex Neighbourhood of the Origin
definitiondef:minkowski-gauge-2026aAnalysisThe gauge of an open convex set U containing 0 in a real normed space assigns to x the infimum of the t > 0 with x/t in U.The Scaling Set of an Open Convex Neighbourhood of the Origin Has an Infimum
lemmalem:minkowski-gauge-existence-2026aAnalysisFor an open convex set U containing 0 in a real normed space and a point x, the set of t > 0 with x/t in U contains every t > ‖x‖/r when the ball of radius r about 0 lies in U, is closed upwards, and so has a nonnegative infimum.Operations Preserving Convexity in : Intersections, Translates, Scalar Multiples, Sums, Affine Images and Preimages, Closure and Interior
lemmalem:convex-sets-operations-rn-2026aAnalysisThe empty set and R^n are convex; intersections of nonempty families of convex sets, translates, scalar multiples, sums and differences of convex sets, images and preimages of convex sets under x -> Ax + b, and the closure and interior of a convex set are convex.Norming Functionals in a Separable Real Normed Space, and the Dual Separates Points
corollarycor:norming-functional-separable-2026aAnalysisIn a separable real normed space every point x has a bounded linear functional F of dual norm at most 1 with F(x) = ‖x‖, of dual norm exactly 1 when the space is not {0}; hence bounded linear functionals separate points.Convex Combinations: Small Cases, Splitting Off the Last Point, Dropping a Zero Weight, Joining Two Combinations, and Membership in Convex Sets
lemmalem:convex-combination-properties-2026bAnalysisConvex combinations of one and two points, the reduction of a combination of N+1 points to a segment point between a combination of N points and the last point, removal of a point of weight zero, the combination obtained by joining two combinations, and closure of convex sets und…Convex Weights, the Standard Simplex, and Convex Combinations in
definitiondef:convex-combination-rn-2026bAnalysisDefines convex weights of length N, the standard simplex of all of them, and the convex combination of N points of R^n with given weights.- Standing notation for convex sets in R^n: segments and convex sets, finite sums of points, closure and interior, with the Heine-Borel theorem as background.
The Hahn–Banach Theorem in a Separable Real Normed Space
theoremthm:hahn-banach-separable-2026aAnalysisIn a separable real normed space, a linear functional on a linear subspace that is dominated by a sublinear functional p ≤ C‖·‖ extends to a bounded linear functional on the whole space that is still dominated by p.- A linear functional dominated by a sublinear functional on a linear subspace M extends to M + ℝx₀ for a point x₀ outside M, by assigning to x₀ the canonical value c given by a supremum; the extension is still dominated.
Elementary Properties of Sublinear Functionals
lemmalem:sublinear-functional-properties-2026aAnalysisA sublinear functional vanishes at 0 and satisfies −p(−x) ≤ p(x), and so does every linear functional it dominates; the norm is sublinear; and a sublinear functional bounded by C‖·‖ is Lipschitz with constant C and bounds the linear functionals below it by C‖·‖.Lipschitz Extension of a Real Function from a Subset of a Metric Space
lemmalem:lipschitz-extension-subset-2026aAnalysisA real function that is Lipschitz with constant L on a nonempty subset of a metric space extends to the whole space with the same constant.- A real-valued function on a real vector space is sublinear if it is subadditive and positively homogeneous.
- A subset of a real vector space is convex if it contains tx+(1−t)y for any two of its points x, y and every t in [0,1].
- A metric space is separable if it has a countable dense subset; a real normed space is separable if it is separable for its norm metric.
- A subset of a metric space is dense if it meets every open ball.
- The dual norm of a bounded linear functional on a real normed space is the infimum of its nonnegative bounds.
The Nonnegative Bounds of a Bounded Linear Functional Have an Infimum, Which Is a Bound
lemmalem:dual-norm-existence-2026aAnalysisFor a bounded linear functional on a real normed space, the set of its nonnegative bounds is nonempty and bounded below by 0, so it has an infimum, and this infimum is itself a bound.