case pos
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
⊢ restrict (c • v) i = c • restrict v i

case neg
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ restrict (c • v) i = c • restrict v i
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
⊢ restrict (c • v) i = c • restrict v i
by_cases hi : MeasurableSet i
case pos.h
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑(restrict (c • v) i) j = ↑(c • restrict v i) j
case pos
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
⊢ restrict (c • v) i = c • restrict v i
ext j
case pos.h
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (c • v) i) j = ↑(c • restrict v i) j
case pos.h
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑(restrict (c • v) i) j = ↑(c • restrict v i) j
intro hj
no goals
case pos.h
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (c • v) i) j = ↑(c • restrict v i) j
simp [restrict_apply _ hi hj]
case neg
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ 0 = c • 0
case neg
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ restrict (c • v) i = c • restrict v i
simp only [restrict_not_measurable _ hi]
case neg.h
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑0 j = ↑(c • 0) j
case neg
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
⊢ 0 = c • 0
ext j
no goals
case neg.h
α : Type u_1
β : Type ?u.514959
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_3
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑0 j = ↑(c • 0) j
simp