no goals
X : Type u_1
Y : Type ?u.1584
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U : Set X
x : X
hU : IsOpen U
⊢ ↑↑μ U = 0 ↔ U = ∅
simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using
  not_congr (hU.measure_pos_iff μ)