Commit 2026-01-26 09:20 1029c45b

View on Github →

feat: more basic API on vector measures (#34414) Cherry picked from #34055.

Estimated changes

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

added def MeasureTheory.VectorMeasure.dirac

added theorem MeasureTheory.VectorMeasure.dirac_apply_of_mem

added theorem MeasureTheory.VectorMeasure.dirac_apply_of_notMem

added theorem MeasureTheory.VectorMeasure.of_biUnion_finset

added theorem MeasureTheory.VectorMeasure.of_compl

added theorem MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat

added theorem MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat