Theorems · Theorem · measure theory

MeasureTheory.innerRegularWRT_isCompact_isClosed

∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [OpensMeasurableSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed

Defined in

Mathlib.MeasureTheory.Measure.RegularityCompacts

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceSecondCountableTopologyTopologicalSpace.IsCompletelyPseudoMetrizableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure