theorem exists_notMeasurableSet_real : ∃ (E : Set ℝ), ¬MeasurableSet E

By cardinality, there exists a subset of ℝ that is not measurable.

theorem exists_zeroMeasure_notMeasurableSet_of_not_isComplete {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (hIncomplete : ¬μ.IsComplete) : ∃ (E : Set α), μ E = 0 ∧ ¬MeasurableSet E

If a measure is not complete, then there exists a measure-zero set that is not measurable.

theorem isCaratheodory_of_measure_eq_zero {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {E : Set α} (hE_zero : μ E = 0) : μ.IsCaratheodory E

Any measure-zero set is Carathéodory measurable for the outer measure induced by the same measure.

theorem isCaratheodory_implies_nullMeasurable_for_volume {E : Set ℝ} (hE : MeasureTheory.volume.IsCaratheodory E) : MeasureTheory.NullMeasurableSet E MeasureTheory.volume

For Lebesgue outer measure on ℝ, Carathéodory measurability implies null measurability for the associated measure volume.

theorem nonNullMeasurable_of_notAEEq_any_measurable_for_volume {E : Set ℝ} (hNotAEEq : ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

A set that is not almost-everywhere equal to any measurable set is not null measurable for Lebesgue volume.

theorem exists_nonNullMeasurableSet_for_volume_of_exists_notAEEq (hExists : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

A witness that is not almost-everywhere equal to any measurable set yields a global witness that is not null measurable for Lebesgue volume.

theorem exists_nonNullMeasurableSet_volume_Icc_real : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Vitali-type bounded witness in Set.Icc (0 : ℝ) 1 that is not null measurable for Lebesgue measure.