Theorems · Definition · measure theory

MeasureTheory.Measure.InnerRegularWRT

{α : Type u_1} → {x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → Prop) → (Set α → Prop) → Prop

We say that a measure μ is inner regular with respect to predicates p q : Set α → Prop, if for every U such that q U and r < μ U, there exists a subset K ⊆ U satisfying p K of measure greater than r. This definition is used to prove some facts about regular and weakly regular measures without repeating the proofs.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

44 results in Mathlib

Foundations

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