α : Type u_2
β : Type ?u.836823
γ : Type ?u.836826
δ : Type ?u.836829
ι : Type u_1
R : Type ?u.836835
R' : Type ?u.836838
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : Countable ι
U : ι → Set α
hU : (⋃ (i : ι), U i) = univ
H : ∀ (i : ι), ↑↑μ (U i) ≤ 0
⊢ μ = 0
α : Type u_2
β : Type ?u.836823
γ : Type ?u.836826
δ : Type ?u.836829
ι : Type u_1
R : Type ?u.836835
R' : Type ?u.836838
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : Countable ι
U : ι → Set α
hU : (⋃ (i : ι), U i) = univ
hμ : μ ≠ 0
⊢ ∃ i, 0 < ↑↑μ (U i)
contrapose! hμ with H
α : Type u_2
β : Type ?u.836823
γ : Type ?u.836826
δ : Type ?u.836829
ι : Type u_1
R : Type ?u.836835
R' : Type ?u.836838
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : Countable ι
U : ι → Set α
hU : (⋃ (i : ι), U i) = univ
H : ∀ (i : ι), ↑↑μ (U i) ≤ 0
⊢ ↑↑μ (⋃ (i : ι), U i) = 0
α : Type u_2
β : Type ?u.836823
γ : Type ?u.836826
δ : Type ?u.836829
ι : Type u_1
R : Type ?u.836835
R' : Type ?u.836838
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : Countable ι
U : ι → Set α
hU : (⋃ (i : ι), U i) = univ
H : ∀ (i : ι), ↑↑μ (U i) ≤ 0
⊢ μ = 0
rw [← measure_univ_eq_zero, ← hU]
no goals
α : Type u_2
β : Type ?u.836823
γ : Type ?u.836826
δ : Type ?u.836829
ι : Type u_1
R : Type ?u.836835
R' : Type ?u.836838
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : Countable ι
U : ι → Set α
hU : (⋃ (i : ι), U i) = univ
H : ∀ (i : ι), ↑↑μ (U i) ≤ 0
⊢ ↑↑μ (⋃ (i : ι), U i) = 0
exact measure_iUnion_null fun i => nonpos_iff_eq_zero.1 (H i)