Theorems · Theorem · measure theory

MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite

∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)}
  (h : μ.FiniteSpanningSetsIn C), MeasureTheory.SigmaFinite μ

If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Cited by

3 results in Mathlib

Foundations

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