α : Type u_1
β : Type ?u.30071
γ : Type ?u.30074
δ : Type ?u.30077
ι : Type ?u.30080
R : Type ?u.30083
R' : Type ?u.30086
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (univ \ s) = ↑↑μ univ - ↑↑μ s
α : Type u_1
β : Type ?u.30071
γ : Type ?u.30074
δ : Type ?u.30077
ι : Type ?u.30080
R : Type ?u.30083
R' : Type ?u.30086
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (sᶜ) = ↑↑μ univ - ↑↑μ s
rw [compl_eq_univ_diff]
no goals
α : Type u_1
β : Type ?u.30071
γ : Type ?u.30074
δ : Type ?u.30077
ι : Type ?u.30080
R : Type ?u.30083
R' : Type ?u.30086
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h₁ : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (univ \ s) = ↑↑μ univ - ↑↑μ s
exact measure_diff (subset_univ s) h₁ h_fin