Theorems · Theorem · measure theory

MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT

∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} [inst : TopologicalSpace 𝓧]
  [OpensMeasurableSpace 𝓧] [MeasureTheory.IsFiniteMeasure μ],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet → MeasureTheory.IsTightMeasureSet {μ}

Finite measures that are inner regular with respect to closed compact sets are tight.

Defined in

Mathlib.MeasureTheory.Measure.Tight

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasure