Theorem MeasureTheory.VectorMeasure.of_iUnion_nonpos
Modification history
2025-04-09 10:22
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
chore: use mixin ordered algebraic typeclasses (part 2) (#20595)
Modified MeasureTheory.VectorMeasure.of_iUnion_nonposView on Github →