Theorems · Theorem · measure theory

MeasureTheory.innerRegularWRT_of_exists_compl_lt

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : Set α → Prop},
  (∀ (A B : Set α), p A → q B → p (A ∩ B)) → (∀ (ε : ENNReal), 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε) → μ.InnerRegularWRT p q

If predicate p is preserved under intersections with sets satisfying predicate q, and sets satisfying p cover the space arbitrarily well, then μ is inner regular with respect to predicates p and q.

Defined in

Mathlib.MeasureTheory.Measure.RegularityCompacts

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace