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.
Continuous functions on Euclidean spaces are Borel measurable
Statement
Assume the Axiom of Countable Choice. Let . Every continuous map is Borel measurable in the sense of Borel measurable and Lebesgue measurable functions on .
Facts & Assumptions
Given: The Axiom of Countable Choice, natural numbers , and a continuous function .
A continuous map has Borel preimages of Borel sets. (A continuous map has Borel preimages of Borel sets)
Proof
Let be Borel. By [L1], the preimage [L1] is a Borel subset of .
By the definition of Borel measurability on Euclidean spaces, step 1.1 says [step 1.1] exactly that is Borel measurable.
Depends on
Used by
- Positive-degree Dolbeault vanishing on pseudoconvex domains Corollary
- Point evaluation is unbounded below the Sobolev continuity threshold Counterexample
- The critical Riesz potential can diverge and be essentially unbounded Counterexample
- Hᵖ atoms with a prescribed moment order Definition
- Involution on L1 of a locally compact group Definition
- Standard normal and normal laws Definition
- The one-dimensional torus and its normalized Haar integral Definition
- The standard intertwining operator A(nu) Definition
- A clipped affine function keeps its zero region Example
- Dilation determines the Riesz-potential target exponent Example
- Hilbert transform of the line Poisson kernel Example
- Matching C¹ pieces across a hyperplane have no jump derivative Example
- Sharp Sobolev threshold for a radial power Example
- The absolute value has a weak first derivative Example
- The positive-type Gaussian on the real line and its cyclic model Example
- Monomial integrals on the sphere and orthonormality on the distinguished torus Lemma
- Monomials form complete orthogonal systems of the Bergman spaces of the disc, the ball and the polydisc Lemma
- Near and far bounds for a Riesz potential Lemma
- The sine integral under Countable Choice: uniform bounds and the value pi/2 Lemma
- The standard normal density has total mass one Lemma
- Chain rule for a C¹ function with bounded derivative Theorem
- Chain rule for globally Lipschitz scalar maps of Sobolev functions Theorem
- For a continuous integrand, the Riemann-Stieltjes and Lebesgue-Stieltjes integrals agree Theorem
- Hardy–Littlewood–Sobolev fractional integration inequality Theorem
Dependency tree · two levels
9 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
- Sheldon Axler, Measure, Integration and Real Analysis, Section 2B (standard reference, not scraped)