Theorems · Theorem · measure theory

MeasureTheory.Content.borel_le_caratheodory

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G]
  [BorelSpace G], S ≤ μ.outerMeasure.caratheodory

For the outer measure coming from a content, all Borel sets are measurable.

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1SpaceMeasurableSpaceBorelSpace