Alphabeta MathHow 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.
Measures are monotone
Statement
Let be a measure on . If and , then .
Facts & Assumptions
Given: A measure on and measurable sets .
A measure is nonnegative and countably additive on pairwise disjoint measurable sequences (Measures on sigma-algebras).
Proof
The sets and are measurable, disjoint, and have union .
Countable additivity applied to these two sets and empty sets thereafter gives ; no subtraction is used, so the argument also covers and the degenerate cases and .
Depends on
Used by
- Measure of a set difference when the smaller set has finite measure Proposition
- Null sets are closed under countable unions and, in a complete space, under arbitrary subsets Proposition
- Sets whose symmetric difference is null have the same measure Proposition
- Assuming countable choice, the semifinite part is a semifinite measure and equals the original measure exactly when it is semifinite Theorem
- Finite and countable subadditivity of measures Theorem
- The first Borel-Cantelli lemma for measures Theorem
- The limsup of the measures is at most the measure of the set limsup under a finite-union bound Theorem
- The measure of a set liminf is at most the liminf of the measures Theorem
Dependency tree · two levels
4 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)