Theorems · Theorem · measure theory

MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular

∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} (s : μ.FiniteSpanningSetsIn {U | IsOpen U ∧ (μ.restrict U).OuterRegular}),
  μ.OuterRegular

If a measure μ admits finite spanning open sets such that the restriction of μ to each set is outer regular, then the original measure is outer regular as well.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpace