Operations on vector measures #
The evaluation lemma for MeasureTheory.VectorMeasure.mapRangeL, the vector measure obtained by
applying a continuous linear map to the values of a vector measure.
Main declarations #
MeasureTheory.VectorMeasure.mapRangeL_apply:mapRangeL f v s = f (v s).
@[simp]
theorem
MeasureTheory.VectorMeasure.mapRangeL_apply
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
{R : Type u_4}
[MeasurableSpace α]
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
[ContinuousAdd M]
[ContinuousConstSMul R M]
[TopologicalSpace N]
[AddCommMonoid N]
[Module R N]
[ContinuousAdd N]
[ContinuousConstSMul R N]
(f : M →L[R] N)
(v : VectorMeasure α M)
(s : Set α)
: