no goals
α : Type u_1
β : Type ?u.3763501
γ : Type ?u.3763504
δ : Type ?u.3763507
ι : Type ?u.3763510
R : Type ?u.3763513
R' : Type ?u.3763516
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
hs : IsCompact s
⊢ (∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ ↑↑μ t = 0) → ↑↑μ s = 0
simpa only [← compl_mem_ae_iff] using hs.compl_mem_sets_of_nhdsWithin