Theorem MeasureTheory.VectorMeasure.dirac_apply_of_mem

Modification history

2026-06-16 01:11
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat(MeasureTheory): use `Is*Apply` for `VectorMeasure` (#40450) …
Modified MeasureTheory.VectorMeasure.dirac_apply_of_memView on Github →
2026-01-26 09:20
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat: more basic API on vector measures (#34414) …
Added MeasureTheory.VectorMeasure.dirac_apply_of_memView on Github →