Theorem MeasureTheory.preVariation.exists_Finpartition_sum_ge'

Modification history

2026-06-04 12:13
Mathlib/MeasureTheory/Measure/PreVariation.lean
feat: more API for the variation of vector measures (#40188)
Added MeasureTheory.preVariation.exists_Finpartition_sum_ge'View on Github →