α : Type u_1
β : Type ?u.41414
m : MeasurableSpace α
M : Type ?u.41420
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0
α : Type u_1
β : Type ?u.41414
m : MeasurableSpace α
M : Type ?u.41420
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s (A ∪ B) = 0
⊢ ↑s A = 0
rw [of_union h hA₁ hB₁] at hAB
no goals
α : Type u_1
β : Type ?u.41414
m : MeasurableSpace α
M : Type ?u.41420
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0
linarith