Theorems · Theorem · measure theory

MeasureTheory.Measure.nullMeasurableSet_compl_support

∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], MeasureTheory.NullMeasurableSet μ.supportᶜ μ

Under the assumption OpensMeasurableSpace, this is redundant because the complement of the support is open, and therefore measurable.

Defined in

Mathlib.MeasureTheory.Measure.Support

Cited by

1 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceMeasurableSpaceHereditarilyLindelofSpace