Def MeasureTheory.VectorMeasure.mapRangeₗ

Modification history

2026-08-24 11:13
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
refactor: change mapRangeₗ to require a `ContinuousLinearMap` (#42767) …
Deleted MeasureTheory.VectorMeasure.mapRangeₗView on Github →
2026-06-04 12:13
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
feat: more API for the variation of vector measures (#40188)
Modified MeasureTheory.VectorMeasure.mapRangeₗView on Github →
2023-05-29 08:45
Mathlib/MeasureTheory/Measure/VectorMeasure.lean
feat: port MeasureTheory.Measure.VectorMeasure (#4016)
Added MeasureTheory.VectorMeasure.mapRangeₗView on Github →