Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Lebesgue Measure of a Lipschitz Image of a Compact Subset of
lemmalem:lipschitz-image-compact-lebesgue-bound-2026aAnalysisMultivariable CalculusIf is Lipschitz with constant on a nonempty compact subset of with values in , then the image of is compact and its Lebesgue measure is at most times that of .Uniform Grids on a Half-Open Box and Grid Hulls of a Compact Set in
lemmalem:grid-hull-compact-rn-2026aAnalysisMultivariable CalculusPartitions a half-open box of into congruent half-open cells of prescribed measure and diameter, shows that halving the mesh refines the partition, and shows that the unions of the cells meeting a compact subset decrease to it with Lebesgue measures converging to i…Local Lipschitz Bound and Continuity for a Semiconvex Function on an Open Convex Set
lemmalem:semiconvex-locally-lipschitz-2026aAnalysisMultivariable CalculusA semiconvex function on an open convex subset of Euclidean space is Lipschitz on a closed ball around each of its points, and is therefore continuous, in the explicit epsilon-delta form used by the extreme value theorem.Subdifferential of a Real-Valued Function on a Convex Subset of
definitiondef:subdifferential-convex-rn-2026aAnalysisMultivariable CalculusDefines the subdifferential of a real-valued function on a convex subset of Euclidean space at a point as the set of vectors whose associated affine function minorises the function and agrees with it at that point, and calls its elements subgradients.- Standing hypotheses for a nonempty bounded open subset of Euclidean space: its closure is compact, and its boundary is the complement of the domain in the closure.
- Standing notation and background facts for second-order equations on open subsets of Euclidean space: the reals, Euclidean space with its metric and topology, symmetric matrices with the positive semidefinite ordering, functions of class with their gradients and Hessians, a…
A Continuous Function on a Closed Interval is Riemann Integrable
corollarycor:continuous-implies-riemann-integrable-2026aAnalysisA function continuous on a closed real interval is Riemann integrable there, and so is its restriction to every nondegenerate closed subinterval. This records, as a citable statement, the integrability already established inside the first part of the fundamental theorem of calcul…Uniqueness of the Limit of a Real Function at a Point of an Interval
lemmalem:limit-function-unique-2026aAnalysisPunctured neighbourhoods of a point of an interval containing at least two points are nonempty, and consequently at most one real number satisfies the defining condition of the limit, so the limit notation is well defined.Constant Sequences and Index-Shifted Sequences of Real Numbers
lemmalem:constant-and-shifted-sequences-2026aAnalysisA constant real sequence converges to its value, and shifting the index of a convergent real sequence by one leaves the limit unchanged.Continuity of the Identity Map, of Powers, and of Polynomial Functions on a Subset of the Real Line
lemmalem:continuity-identity-polynomial-real-2026aAnalysisThe identity map, the natural-number power maps, and the restriction of any polynomial function are continuous on every subset of the real line.Basic Facts about Intervals of the Real Line and Their Interior Points
lemmalem:real-interval-basic-facts-2026aAnalysisCollects the routine facts about intervals used throughout single-variable calculus: that the real line is an interval all of whose points are interior, that closed intervals between points of an interval lie inside it, and that open and closed intervals are intervals with the ex…A Continuous Injective Function on a Closed Interval is Strictly Monotone
problemprob:continuous-injective-strictly-monotone-2026aAnalysisAnalysis level. Injectivity plus continuity on a closed real interval forces strict monotonicity; the whole argument is repeated use of the intermediate value theorem.A Nonnegative Continuous Function with Zero Integral
problemprob:nonnegative-zero-integral-2026aAnalysisHonours to analysis level. A continuous nonnegative function on a closed interval whose integral vanishes is identically zero.A Function with Small Derivative Has Exactly One Fixed Point
problemprob:contraction-unique-fixed-point-2026aAnalysisHonours level. A function differentiable on the whole real line whose derivative is bounded in absolute value by one half has exactly one fixed point.- Honours level. Show that the sequence given by and is increasing and bounded above by , hence convergent, and that its limit is .
- Introductory to honours level. A continuous function on the unit interval taking equal values at the endpoints takes equal values at some pair of points half a unit apart.
- Introductory calculus. Show that has exactly one real zero and locate it in the open interval from to , combining the intermediate value theorem with strict monotonicity from the sign of the derivative.
The Rectangle of Greatest Area with a Given Perimeter
problemprob:rectangle-maximal-area-2026aAnalysisIntroductory calculus. Show that the area function of a rectangle of fixed perimeter attains a greatest value on the relevant closed interval and does so only at the square, using the extreme value theorem and the vanishing of the derivative at an interior extremum.A Limit Computed from the Epsilon-Delta Definition
problemprob:limit-square-epsilon-delta-2026aAnalysisBeginner level. Verify the limit of at straight from the epsilon-delta definition, by exhibiting a delta for each epsilon.- A function continuous on an interval and differentiable at its interior points is nondecreasing when its derivative is nonnegative there and strictly increasing when its derivative is positive, with the corresponding statements for the reverse inequalities.