Theorem MeasureTheory.VectorMeasure.ennrealToMeasure_zero

Modification history

2026-09-03 15:14

Mathlib/MeasureTheory/VectorMeasure/Basic.lean

chore(MeasureTheory/VectorMeasure): split long file Basic.lean (#43271) …

Modified MeasureTheory.VectorMeasure.ennrealToMeasure_zero View on Github →

2026-04-08 09:27

Mathlib/MeasureTheory/VectorMeasure/Basic.lean

feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation (#26160) …

Added MeasureTheory.VectorMeasure.ennrealToMeasure_zero View on Github →