Theorems · Theorem · measure theory

MeasureTheory.tendsto_measure_sigmaFiniteSetGE

∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν],
  Filter.Tendsto (fun n => ν (μ.sigmaFiniteSetGE ν n)) Filter.atTop
    (nhds (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s))

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure