α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
⊢ ↑↑ν (toMeasurable μ sᶜ) = 0
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
⊢ μ ⟂ₘ ν
use toMeasurable μ s, measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans hs
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ toMeasurable μ sᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
⊢ ↑↑ν (toMeasurable μ sᶜ) = 0
refine' measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx _) ht
no goals
α : Type u_1
m0 : MeasurableSpace α
μ μ₁ μ₂ ν ν₁ ν₂ : Measure α
s t : Set α
hs : ↑↑μ s = 0
ht : ↑↑ν t = 0
hst : univ ⊆ s ∪ t
x : α
hx : x ∈ toMeasurable μ sᶜ
hxs : x ∈ s
⊢ x ∈ toMeasurable μ s
exact subset_toMeasurable _ _ hxs