α : Type u_1
β : Type ?u.732836
γ : Type ?u.732839
δ : Type ?u.732842
ι : Type ?u.732845
R : Type ?u.732848
R' : Type ?u.732851
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), ↑↑μ (s ∩ spanningSets μ n) = 0) ↔ ↑↑μ (⋃ (n : ℕ), s ∩ spanningSets μ n) = 0
α : Type u_1
β : Type ?u.732836
γ : Type ?u.732839
δ : Type ?u.732842
ι : Type ?u.732845
R : Type ?u.732848
R' : Type ?u.732851
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), ↑↑μ (s ∩ spanningSets μ n) = 0) ↔ ↑↑μ s = 0
nth_rw 2 [show s = ⋃ n, s ∩ spanningSets μ n by
    rw [← inter_iUnion, iUnion_spanningSets, inter_univ] ]
no goals
α : Type u_1
β : Type ?u.732836
γ : Type ?u.732839
δ : Type ?u.732842
ι : Type ?u.732845
R : Type ?u.732848
R' : Type ?u.732851
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), ↑↑μ (s ∩ spanningSets μ n) = 0) ↔ ↑↑μ (⋃ (n : ℕ), s ∩ spanningSets μ n) = 0
rw [measure_iUnion_null_iff]
no goals
α : Type u_1
β : Type ?u.732836
γ : Type ?u.732839
δ : Type ?u.732842
ι : Type ?u.732845
R : Type ?u.732848
R' : Type ?u.732851
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ s = ⋃ (n : ℕ), s ∩ spanningSets μ n
rw [← inter_iUnion, iUnion_spanningSets, inter_univ]