Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Let be a measure space. For , the indicator function is defined by for and otherwise. A simple function on is a measurable function…
Measurable Function and Real-Valued Measurable Function
definitiondef:measurable-function-2026bAnalysisProbabilityLet and be measurable spaces. A function is measurable (with respect to and ) if for every . A real-valued function is called measurable if it…Existence of Lebesgue Measure on the Real Line
theoremthm:lebesgue-measure-real-line-2026aAnalysisProbabilityLet be the Lebesgue outer measure on the real line. Then: 1. is an outer measure on ; 2. every Borel set is Carathéodory measurable with respect to ; 3. consequently, by Caratheodory Extension Theorem, the restriction…Lebesgue Outer Measure on the Real Line
definitiondef:lebesgue-outer-measure-real-line-2026aAnalysisProbabilityFor a subset of the real line , the Lebesgue outer measure of is where the infimum is taken over all sequences of open intervals …- Let be a set and let be an outer measure on . Let be the family of all subsets of that are Carathéodory measurable with respect to , in the sense of that definition. Then: 1. is a -algebra on ; 2. the restricti…
- Let be a set. An outer measure on is a function from the family of all subsets of to (with the conventions of Measure, Measure Space, and Probability Measure) such that: 1. ; 2. (monotonicity) if…
Measure, Measure Space, and Probability Measure
definitiondef:measure-measure-space-2026aAnalysisProbabilityLet be a measurable space. Write for the set , where is a formal symbol with the conventions for all , for all real , and…Borel Sigma-Algebra on the Real Line
definitiondef:borel-sigma-algebra-real-line-2026aAnalysisProbabilityIdentify the real line with the Euclidean space . The Borel -algebra on , denoted , is the -algebra generated by the family of all open subsets of . Its members are called Borel sets. In…- Let be a set and let be a family of subsets of . The -algebra generated by , denoted , is the family of those subsets of that belong to every -algebra on containing .
Sigma-Algebra and Measurable Space
definitiondef:sigma-algebra-measurable-space-2026aAnalysisProbabilityLet be a set. A -algebra on is a family of subsets of with the following three properties. 1. . 2. If , then the complement belongs to . 3. For every sequence …Integral of a Smooth n-Form over a Compact Oriented Smooth Manifold with Boundary
definitiondef:integral-form-oriented-manifold-boundary-2026aAnalysisGeometryMultivariable CalculusLet and let be an oriented smooth manifold with boundary of dimension that is compact in the sense of Smooth Atlas and Smooth Manifold with Boundary, with chosen oriented smooth atlas , and write…Independence of the Manifold Integral from Chart and Partition Choices
theoremthm:integral-manifold-independence-choices-2026aAnalysisGeometryMultivariable CalculusLet and let be an oriented smooth manifold with boundary of dimension that is compact in the sense of Smooth Atlas and Smooth Manifold with Boundary, with chosen oriented smooth atlas , and write…Smooth Partitions of Unity on a Compact Smooth Manifold with Boundary
theoremthm:smooth-partition-unity-compact-manifold-boundary-2026aAnalysisTopologyGeometryLet be a smooth manifold with boundary that is compact in the sense of that definition, with chosen smooth atlas . Then there exist , indices , and smooth differential -forms…Existence of Smooth Bump Functions on Euclidean Space
lemmalem:smooth-bump-function-euclidean-2026aAnalysisMultivariable CalculusLet , let be a point of Euclidean space , and let with . Then there exists a smooth map such that, with denoting the Euclidean distance on : 1. …Pullback Invariance of the Integral under Orientation-Preserving Smooth Diffeomorphisms
theoremthm:pullback-invariance-integral-diffeomorphism-euclidean-2026bAnalysisGeometryMultivariable CalculusLet , let be admissible domains in Euclidean space in the sense of Continuous n-Form, Support, and Zero Extension on a Euclidean or Half-Space Domain, and let be an orientation-preserving…Integral of a Compactly Supported Continuous n-Form on a Euclidean or Half-Space Domain
definitiondef:integral-compactly-supported-n-form-euclidean-2026aAnalysisMultivariable CalculusLet , let be an admissible domain in Euclidean space with ambient set in the sense of Continuous n-Form, Support, and Zero Extension on a Euclidean or Half-Space Domain, and let be a continuous differential -form on…Zero Extension Continuity and Box Independence of the Iterated Integral
lemmalem:zero-extension-box-integral-euclidean-2026aAnalysisMultivariable CalculusLet , let be an admissible domain in Euclidean space with ambient set in the sense of Continuous n-Form, Support, and Zero Extension on a Euclidean or Half-Space Domain, and let be a continuous differential -form on…Continuous n-Form, Support, and Zero Extension on a Euclidean or Half-Space Domain
definitiondef:continuous-n-form-support-euclidean-domain-2026cAnalysisMultivariable CalculusDefines admissible domains (open subsets of R^n or relatively open subsets of the closed upper half-space), differential n-forms on them with their coefficient functions, continuity, support, compact support, and the zero extension of the coefficient function.Stokes Theorem for Compact Oriented Smooth Manifolds with Boundary
theoremthm:stokes-smooth-manifold-boundary-2026aAnalysisTopologyGeometryMultivariable CalculusLet with , and let be an oriented smooth manifold with boundary of dimension that is compact as defined in Smooth Atlas and Smooth Manifold with Boundary. Let be a smooth differential -form on and let denote the…- Defines Cauchy sequences in a metric space: terms with large enough indices are arbitrarily close to one another.