case intro.intro.intro
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₂ : v₂ ⟂ᵥ w
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₁ : v₁ ⟂ᵥ w
h₂ : v₂ ⟂ᵥ w
⊢ v₁ + v₂ ⟂ᵥ w
obtain ⟨u, hmu, hu₁, hu₂⟩ := h₁
case intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w
case intro.intro.intro
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₂ : v₂ ⟂ᵥ w
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w
obtain ⟨v, hmv, hv₁, hv₂⟩ := h₂
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ u ∩ v
x✝ : MeasurableSet t
⊢ ↑(v₁ + v₂) t = 0

case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ (u ∩ v)ᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0
case intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w
refine' mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => _) fun t ht hmt => _
no goals
case intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ u ∩ v
x✝ : MeasurableSet t
⊢ ↑(v₁ + v₂) t = 0
rw [add_apply, hu₁ _ (Set.subset_inter_iff.1 ht).1, hv₁ _ (Set.subset_inter_iff.1 ht).2,
  zero_add]
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ (u ∩ v)ᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0
rw [Set.compl_inter] at ht
case intro.intro.intro.intro.intro.intro.refine'_2.x
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ vᶜ \ uᶜ ∩ t ⊆ vᶜ

case intro.intro.intro.intro.intro.intro.refine'_2.x
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ uᶜ ∩ t ⊆ uᶜ

α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)

α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
case intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0
rw [(_ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t),
  of_union _ (hmu.compl.inter hmt) ((hmv.compl.diff hmu.compl).inter hmt), hu₂, hv₂, add_zero]
no goals
case intro.intro.intro.intro.intro.intro.refine'_2.x
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ vᶜ \ uᶜ ∩ t ⊆ vᶜ
exact Set.Subset.trans (Set.inter_subset_left _ _) (Set.diff_subset _ _)
no goals
case intro.intro.intro.intro.intro.intro.refine'_2.x
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ uᶜ ∩ t ⊆ uᶜ
exact Set.inter_subset_left _ _
no goals
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)
exact disjoint_sdiff_self_right.mono (Set.inter_subset_left _ _) (Set.inter_subset_left _ _)
case h₁
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

case h₂
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
⊢ x ∈ t
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
apply Set.Subset.antisymm <;> intro x hx
case pos
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

case neg
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
case h₁
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
by_cases hxu' : x ∈ uᶜ
case neg.inl
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
hxu : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

case neg.inr
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
hxv : x ∈ vᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
case neg
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
rcases ht hx with (hxu | hxv)
no goals
case neg.inl
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
hxu : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

case neg.inr
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : ¬x ∈ uᶜ
hxv : x ∈ vᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]
no goals
case pos
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
exact Or.inl ⟨hxu', hx⟩
no goals
case h₂
α : Type u_3
β : Type ?u.661519
m : MeasurableSpace α
L : Type ?u.661525
M : Type u_2
N : Type u_1
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
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ (t : Set α), t ⊆ u → ↑v₁ t = 0
hu₂ : ∀ (t : Set α), t ⊆ uᶜ → ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ (t : Set α), t ⊆ v → ↑v₂ t = 0
hv₂ : ∀ (t : Set α), t ⊆ vᶜ → ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
⊢ x ∈ t
cases' hx with hx hx <;> exact hx.2