α : Type u_1
β : Type ?u.733391
γ : Type ?u.733394
δ : Type ?u.733397
ι : Type ?u.733400
R : Type ?u.733403
R' : Type ?u.733406
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (¬∃ n, 0 < ↑↑μ (s ∩ spanningSets μ n)) ↔ ¬0 < ↑↑μ s
α : Type u_1
β : Type ?u.733391
γ : Type ?u.733394
δ : Type ?u.733397
ι : Type ?u.733400
R : Type ?u.733403
R' : Type ?u.733406
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∃ n, 0 < ↑↑μ (s ∩ spanningSets μ n)) ↔ 0 < ↑↑μ s
rw [← not_iff_not]
α : Type u_1
β : Type ?u.733391
γ : Type ?u.733394
δ : Type ?u.733397
ι : Type ?u.733400
R : Type ?u.733403
R' : Type ?u.733406
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (x : ℕ), ↑↑μ (s ∩ spanningSets μ x) = 0) ↔ ↑↑μ s = 0
α : Type u_1
β : Type ?u.733391
γ : Type ?u.733394
δ : Type ?u.733397
ι : Type ?u.733400
R : Type ?u.733403
R' : Type ?u.733406
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (¬∃ n, 0 < ↑↑μ (s ∩ spanningSets μ n)) ↔ ¬0 < ↑↑μ s
simp only [not_exists, not_lt, nonpos_iff_eq_zero]
no goals
α : Type u_1
β : Type ?u.733391
γ : Type ?u.733394
δ : Type ?u.733397
ι : Type ?u.733400
R : Type ?u.733403
R' : Type ?u.733406
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (x : ℕ), ↑↑μ (s ∩ spanningSets μ x) = 0) ↔ ↑↑μ s = 0
exact forall_measure_inter_spanningSets_eq_zero s