Theorems · Theorem · real analysis

intervalIntegral.FTCFilter.finiteAt_inner

∀ {a : ℝ} (l : Filter ℝ) {l' : Filter ℝ} [h : intervalIntegral.FTCFilter a l l'] {μ : MeasureTheory.Measure ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ], μ.FiniteAtFilter l'

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

4 results in Mathlib

Foundations

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

Assumes

intervalIntegral.FTCFilterMeasureTheory.IsLocallyFiniteMeasure