Theorems · Theorem · measure theory

Set.measure_eq_iInf_isOpen

∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α)
  [μ.OuterRegular], μ A = ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U

For an outer regular measure, the measure of a set is the infimum of the measures of open sets containing it.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceMeasureTheory.Measure.OuterRegular