case intro.intro.intro
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
⊢ -v ⟂ᵥ w
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ⟂ᵥ w
⊢ -v ⟂ᵥ w
obtain ⟨u, hmu, hu₁, hu₂⟩ := h
case intro.intro.intro
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑(-v) s = 0
case intro.intro.intro
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
⊢ -v ⟂ᵥ w
refine' ⟨u, hmu, fun s hs => _, hu₂⟩
case intro.intro.intro
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑v s = 0
case intro.intro.intro
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑(-v) s = 0
rw [neg_apply v s, neg_eq_zero]
no goals
case intro.intro.intro
α : Type u_2
β : Type ?u.681547
m : MeasurableSpace α
L : Type ?u.681553
M✝ : Type ?u.681556
N : Type u_3
inst✝⁸ : AddCommMonoid L
inst✝⁷ : TopologicalSpace L
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : TopologicalSpace M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
v✝ v₁ v₂ : VectorMeasure α M✝
w✝ w₁ w₂ : VectorMeasure α N
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
s : Set α
hs : s ⊆ u
⊢ ↑v s = 0
exact hu₁ s hs