Theorems · Inductive type · measure theory

MeasureTheory.Measure.MeasureDense

{X : Type u_1} → [m : MeasurableSpace X] → MeasureTheory.Measure X → Set (Set X) → Prop

A family 𝒜 of sets of a measure space is said to be measure-dense if it contains only measurable sets and can approximate any measurable set with finite measure, in the sense that for any measurable set s with finite measure the symmetric difference s ∆ t can be made arbitrarily small when t ∈ 𝒜. We show below that such a family can be chosen to contain only sets with finite measure. The term "measure-dense" is justified by the fact that the approximating condition translates to the usual notion of density in the metric space made by constant indicators of measurable sets equipped with the Lᵖ norm.

Defined in

Mathlib.MeasureTheory.Measure.SeparableMeasure

Cited by

13 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

MeasurableSpace