Theorems · Definition · measure theory

MeasureTheory.Measure.sigmaFiniteSetGE

{α : Type u_1} →
  {mα : MeasurableSpace α} →
    MeasureTheory.Measure α → (ν : MeasureTheory.Measure α) → [MeasureTheory.IsFiniteMeasure ν] → ℕ → Set α

A measurable set such that μ.restrict (μ.sigmaFiniteSetGE ν n) is sigma-finite and for C the supremum of ν s over all measurable sets s with μ.restrict s sigma-finite, ν (μ.sigmaFiniteSetGE ν n) ≥ C - 1/n.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Cited by

8 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure