case pos
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
⊢ map (c • v) f = c • map v f

case neg
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ map (c • v) f = c • map v f
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
⊢ map (c • v) f = c • map v f
by_cases hf : Measurable f
case pos.h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
⊢ MeasurableSet i → ↑(map (c • v) f) i = ↑(c • map v f) i
case pos
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
⊢ map (c • v) f = c • map v f
ext i
case pos.h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map (c • v) f) i = ↑(c • map v f) i
case pos.h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
⊢ MeasurableSet i → ↑(map (c • v) f) i = ↑(c • map v f) i
intro hi
no goals
case pos.h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ ↑(map (c • v) f) i = ↑(c • map v f) i
simp [map_apply _ hf hi]
case neg
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ 0 = c • 0
case neg
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ map (c • v) f = c • map v f
simp only [map, dif_neg hf]
case neg.h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
i : Set β
⊢ MeasurableSet i → ↑0 i = ↑(c • 0) i
case neg
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ 0 = c • 0
ext i
no goals
case neg.h
α : Type u_1
β : Type u_3
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
i : Set β
⊢ MeasurableSet i → ↑0 i = ↑(c • 0) i
simp