Def MeasureTheory.VectorMeasure.mapRangeL

Modification history

2026-09-03 15:14
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
chore(MeasureTheory/VectorMeasure): split long file Basic.lean (#43271) …
Modified MeasureTheory.VectorMeasure.mapRangeLView on Github →
2026-08-24 11:13
Mathlib/MeasureTheory/VectorMeasure/Basic.lean
refactor: change mapRangeₗ to require a `ContinuousLinearMap` (#42767) …
Added MeasureTheory.VectorMeasure.mapRangeLView on Github →