How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Measure of a set difference when the smaller set has finite measure
Statement
Let be a measure and let be measurable with . Then
If , all terms are real and hence . If , then .
Facts & Assumptions
Given: Measurable sets for a measure , with .
A measure is countably additive on pairwise disjoint measurable sequences (Measures on sigma-algebras).
If are measurable, then (Measures are monotone).
Proof
The disjoint measurable sets and have union , so .
If , monotonicity makes both summands in step 1.1 finite, and cancellation in gives .
If , then cannot be finite, because its sum with the finite number would be finite; hence it is . Together with steps 1.1 and 2.1 this proves every asserted case, including and .
Depends on
Used by
- The indicator of a fat Cantor set is upper semicontinuous and equal almost everywhere to no Riemann integrable function Counterexample
- An open dense set of measure less than 1 is the monotone L¹-limit of Riemann integrable indicators, but its indicator is not Riemann integrable Example
- A finite-measure measurable set in ℝⁿ has a compact core and a bounded open neighbourhood of arbitrarily small excess Lemma
- A finite-measure measurable set in ℝⁿ is approximable in measure by a finite union of boxes Lemma
- Assuming countable choice, an infinite-measure set in a semifinite measure space has arbitrarily large finite-measure subsets Lemma
- Basic identities for a probability measure Lemma
- Finite measures agreeing on a generating pi-system and on the whole space are equal Lemma
- Finite-measure sets are approximable in measure by sets from a countable generating algebra Lemma
- For a Lebesgue measurable set and every positive ε there is an open superset whose difference from it has outer measure below ε Lemma
- Lipschitz curves and dominated interval vector measures Lemma
- Nondentability produces a vector measure without density Lemma
- Assuming countable choice, the Carathéodory extension dominates every other extension and agrees with it on finite-measure sets Proposition
- Positive sets sweep out ergodic probability systems Proposition
- Assuming countable choice, Borel probability measures on Polish spaces are inner regular Theorem
- Assuming countable choice, the Lebesgue measure of a measurable set is the supremum of the measures of its compact subsets Theorem
- Continuity from above when one set has finite measure Theorem
- Continuity from below for measures Theorem
- Direct integrals of measurable Hilbert fields are Hilbert spaces Theorem
- Interval formulas and atoms for a Lebesgue-Stieltjes measure Theorem
- Probability laws correspond to distribution functions Theorem
Dependency tree · two levels
5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- S. Axler, Measure, Integration & Real Analysis, Theorem 2.57 (standard reference, not scraped)