Theorems · Theorem · measure theory

MeasurableSet.measure_eq_iSup_isCompact

∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
  MeasurableSet U → ∀ (μ : MeasureTheory.Measure α) [μ.InnerRegular], μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ K

The measure of a measurable set is the supremum of the measures of compact sets it contains.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceMeasureTheory.Measure.InnerRegular