Theorems · Definition · measure theory

MeasureTheory.toMeasurable

{α : Type u_6} → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Set α → Set α

A measurable set t ⊇ s such that μ t = μ s. It even satisfies μ (t ∩ u) = μ (s ∩ u) for any measurable set u if μ s ≠ ∞, see measure_toMeasurable_inter. This property holds without the assumption μ s ≠ ∞ when the space is s-finite (for example σ-finite); see measure_toMeasurable_inter_of_sFinite. If s is a null measurable set, then we also have t =ᵐ[μ] s, see NullMeasurableSet.toMeasurable_ae_eq. This notion is sometimes called a "measurable hull" in the literature.

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Cited by

77 results in Mathlib

Foundations

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

Assumes

MeasurableSpace