An analytic non-Borel subset of ℝ: the image of the Baire-space witness under the continuous injection. Analyticity transfers along the continuous image; non-Borelness transfers back along the injective preimage.
DeclMeasureTheory.exists_analyticSet_not_measurableSet_real
∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A
TopicAnalytic sets
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6023 | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6023
Cite
Verification
- Library
- ZPM.MeasureTheory.AnalyticMeasurability.NonBorelWitness
- Statement digest
- b7b3031e0292
- First verified
- 2026-09-24T00:00:00Z