case pos
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0

case neg
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
⊢ restrict 0 i = 0
by_cases hi : MeasurableSet i
case pos.h
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑(restrict 0 i) j = ↑0 j
case pos
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ restrict 0 i = 0
ext j
case pos.h
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict 0 i) j = ↑0 j
case pos.h
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
⊢ MeasurableSet j → ↑(restrict 0 i) j = ↑0 j
intro hj
case pos.h
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑0 (j ∩ i) = ↑0 j
case pos.h
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict 0 i) j = ↑0 j
rw [restrict_apply 0 hi hj]
no goals
case pos.h
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑0 (j ∩ i) = ↑0 j
rfl
no goals
case neg
α : Type u_1
β : Type ?u.474705
m inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ restrict 0 i = 0
exact dif_neg hi