Commit 2026-06-16 01:11 94fba23a

View on Github →

feat(MeasureTheory): use Is*Apply for VectorMeasure (#40450) Add FunLike and IsApply instances for VectorMeasure, also add a coe_mk simp lemma.

Estimated changes

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

added theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply

added theorem MeasureTheory.Measure.toSignedMeasure_apply

deleted theorem MeasureTheory.VectorMeasure.add_apply

deleted def MeasureTheory.VectorMeasure.coeFnAddMonoidHom

deleted theorem MeasureTheory.VectorMeasure.coe_add

deleted theorem MeasureTheory.VectorMeasure.coe_finsetSum

deleted theorem MeasureTheory.VectorMeasure.coe_injective

added theorem MeasureTheory.VectorMeasure.coe_mk

deleted theorem MeasureTheory.VectorMeasure.coe_neg

deleted theorem MeasureTheory.VectorMeasure.coe_smul

deleted theorem MeasureTheory.VectorMeasure.coe_sub

deleted theorem MeasureTheory.VectorMeasure.coe_zero

modified theorem MeasureTheory.VectorMeasure.dirac_apply_of_mem

deleted theorem MeasureTheory.VectorMeasure.ext_iff'

deleted theorem MeasureTheory.VectorMeasure.neg_apply

deleted theorem MeasureTheory.VectorMeasure.smul_apply

deleted theorem MeasureTheory.VectorMeasure.sub_apply

deleted theorem MeasureTheory.VectorMeasure.zero_apply

Modified Mathlib/MeasureTheory/VectorMeasure/BoundedVariation.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Integral.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean

Modified Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean