Theorems · Theorem · measure theory

MeasureTheory.Content.contentRegular_exists_compact

∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G),
  μ.ContentRegular →
    ∀ (K : TopologicalSpace.Compacts G) {ε : NNReal}, ε ≠ 0 → ∃ K', K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε

Defined in

Mathlib.MeasureTheory.Measure.Content

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace