α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v A = ↑v (A \ B) + ↑v B
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v B = ↑v A
symm
no goals
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v A = ↑v (A \ B ∪ A ∩ B)
simp only [Set.diff_union_inter]
case h
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A \ B) (A ∩ B)

case hA
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A \ B)

case hB
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B ∪ A ∩ B) = ↑v (A \ B) + ↑v (A ∩ B)
rw [of_union]
case h
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)
case h
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A \ B) (A ∩ B)
rw [disjoint_comm]
no goals
case h
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)
exact Set.disjoint_of_subset_left (A.inter_subset_right B) disjoint_sdiff_self_right
no goals
case hA
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A \ B)
exact hA.diff hB
no goals
case hB
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)
exact hA.inter hB
case h
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)

case hA
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

case hB
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (B \ A)
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v (A ∩ B) = ↑v (A \ B) + ↑v (A ∩ B ∪ B \ A)
rw [of_union, h', add_zero]
no goals
case h
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)
exact Set.disjoint_of_subset_left (A.inter_subset_left B) disjoint_sdiff_self_right
no goals
case hA
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (A ∩ B)
exact hA.inter hB
no goals
case hB
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ MeasurableSet (B \ A)
exact hB.diff hA
no goals
α : Type u_1
β : Type ?u.27702
m : MeasurableSpace α
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
v : VectorMeasure α M
f : ℕ → Set α
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : ↑v (B \ A) = 0
⊢ ↑v (A \ B) + ↑v (A ∩ B ∪ B \ A) = ↑v (A \ B) + ↑v B
rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]