Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero

Filter.Tendsto (fun E => MeasureTheory.volume (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2))
  AbsolutelyContinuousOnInterval.totalLengthFilter (nhds 0)

Defined in: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Cited by: 1 results in Mathlib
Foundations: Depth 246 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites35

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
Finsetstatement · cited by 13,712
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Filterproof · cited by 8,121
nhdsstatement and proof · cited by 5,554
Finset.sumproof · cited by 5,195
Filter.Tendstostatement and proof · cited by 3,814
Set.iUnionstatement and proof · cited by 2,483

Cited by1

Results whose statement or proof uses this declaration.

AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zeroproof · cited by 1