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.
Composition with a Borel measurable outer map preserves measurability
Statement
Let , , and be measurable spaces. If is measurable and is measurable, then is measurable.
In particular, if is measurable and is a Borel measurable function on its codomain, then is measurable.
Facts & Assumptions
Given: Measurable spaces , , , a measurable map , and a measurable map .
Measurability means that preimages of measurable sets are measurable. (A measurable function between measurable spaces)
Proof
Let . Since is measurable, [L1] gives [given, L1] .
Since is measurable, [L1] applied again gives
So is measurable. [step 1.1, L1] ∎
Depends on
Used by
- Positive, negative, and truncated Sobolev functions Corollary
- Sobolev maxima and minima form a lattice Corollary
- Direct integral of a measurable Hilbert field Definition
- Measurable and decomposable operator fields Definition
- The Fourier transform on an LCA group Definition
- The one-dimensional torus and its normalized Haar integral Definition
- A clipped affine function keeps its zero region Example
- The regular representation of the real line as a multiplicity-one integral of characters Example
- Borel representatives make the convolution integrand Borel measurable Lemma
- Diagonal multipliers form a von Neumann algebra Lemma
- Direct integrals transport along bimeasurable base isomorphisms Lemma
- Fourier pairing for a finite measure and Schwartz data Lemma
- Laws commute with measurable maps Lemma
- Measurable cocycle fields for a multiplicity-normalized system Lemma
- Measurable coordinatewise functions preserve independence Lemma
- Measurable dense selections for fields of nonempty compact sets Lemma
- Measurable Gram-Schmidt and constant-field trivializations on dimension strata Lemma
- Measurable sections have measurable pointwise inner products Lemma
- Multiplicity model of a projection-valued measure over a standard Borel base Lemma
- Near and far bounds for a Riesz potential Lemma
- Chain rule for a C¹ function with bounded derivative Theorem
- Chain rule for globally Lipschitz scalar maps of Sobolev functions Theorem
- Change of variables for expectation Theorem
- Convex functions of martingales are submartingales Theorem
- Decomposable operators are the commutant of diagonal multiplication Theorem
- Direct integrals of measurable Hilbert fields are Hilbert spaces Theorem
- Hardy–Littlewood–Sobolev fractional integration inequality Theorem
- Measurable essentially bounded operator fields act decomposably Theorem
- Spectral multiplicity model for separably acting abelian von Neumann algebras Theorem
Dependency tree · two levels
2 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
- John K. Hunter, Measure Theory, Definition 3.3 (standard reference, not scraped)