case pos
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
ht : MeasurableSet t
⊢ ↑v t = 0

case neg
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ ↑v t = 0

case pos
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : MeasurableSet t
⊢ ↑w t = 0

case neg
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ ↑w t = 0
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
⊢ v ⟂ᵥ w
refine' ⟨s, hs, fun t hst => _, fun t hst => _⟩ <;> by_cases ht : MeasurableSet t
no goals
case pos
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
ht : MeasurableSet t
⊢ ↑v t = 0
exact h₁ t hst ht
no goals
case neg
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ ↑v t = 0
exact not_measurable v ht
no goals
case pos
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : MeasurableSet t
⊢ ↑w t = 0
exact h₂ t hst ht
no goals
case neg
α : Type u_1
β : Type ?u.656315
m : MeasurableSpace α
L : Type ?u.656321
M : Type u_2
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
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑v t = 0
h₂ : ∀ (t : Set α), t ⊆ sᶜ → MeasurableSet t → ↑w t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ ↑w t = 0
exact not_measurable w ht