Theorem MeasureTheory.VectorMeasure.dirac_apply_of_notMem

Modification history

2026-01-26 09:20
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat: more basic API on vector measures (#34414) …
Added MeasureTheory.VectorMeasure.dirac_apply_of_notMemView on Github →