no goals
α : Type u_1
β : Type ?u.7681
R : Type ?u.7684
R' : Type ?u.7687
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
S : Set (Set α)
hS : Set.Countable S
⊢ ↑m (⋃₀ S) = 0 ↔ ∀ (s : Set α), s ∈ S → ↑m s = 0
rw [sUnion_eq_biUnion, m.biUnion_null_iff hS]