case pos
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ restrict (v + w) i = restrict v i + restrict w i

case neg
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict (v + w) i = restrict v i + restrict w i
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
⊢ restrict (v + w) i = restrict v i + restrict w i
by_cases hi : MeasurableSet i
case pos.h
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑(restrict (v + w) i) j = ↑(restrict v i + restrict w i) j
case pos
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ restrict (v + w) i = restrict v i + restrict w i
ext j
case pos.h
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (v + w) i) j = ↑(restrict v i + restrict w i) j
case pos.h
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑(restrict (v + w) i) j = ↑(restrict v i + restrict w i) j
intro hj
no goals
case pos.h
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (v + w) i) j = ↑(restrict v i + restrict w i) j
simp [restrict_apply _ hi hj]
no goals
case neg
α : Type u_1
β : Type ?u.487868
m inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v✝ : VectorMeasure α M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict (v + w) i = restrict v i + restrict w i
simp [restrict_not_measurable _ hi]