Existence_of_Non_Measurable_Subset_of_Real_Numbers
Provedmeasure-theoryproofwiki
There exists a subset of the real numbers that is not Lebesgue measurable.
Preamble
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.MeasureTheory.Measure.Lebesgue.Basic theorem Existence_of_Non_Measurable_Subset_of_Real_Numbers : ∃ S : Set ℝ, ¬ MeasurableSet S := by sorry
Source