Mathesis

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

Arguments

DOIAuthorDate
MTH.R-2026-6023Dhruv GuptaDhruv Gupta2026-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