no goals
α : Type u_1
β : Type ?u.3710857
γ : Type ?u.3710860
δ : Type ?u.3710863
ι : Type ?u.3710866
R : Type ?u.3710869
R' : Type ?u.3710872
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝[s] x)
⊢ ↑↑μ ∅ < ⊤
simp