Theorems · Theorem · measure theory

MeasureTheory.measure_sigmaFiniteSetGE_ge

∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν]
  (n : ℕ),
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤
    ν (μ.sigmaFiniteSetGE ν n)

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure