Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero

∀ (a b : ℝ),
  Filter.Tendsto
    (fun E => (MeasureTheory.volume.restrict (Set.uIoc a b)) (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2))
    (AbsolutelyContinuousOnInterval.totalLengthFilter ⊓
      Filter.principal (AbsolutelyContinuousOnInterval.disjWithin a b))
    (nhds 0)

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

1 results in Mathlib

Foundations

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