Theorem: locally_lipschitz_image_of_null_set_is_null_set_open (Sard/LocallyLipschitzMeasureZero.lean)

State before:
X : Type u_1
Y : Type u_2
inst✝⁶ : MetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : MetricSpace Y
inst✝² : MeasurableSpace Y
inst✝¹ : BorelSpace Y
inst✝ : SigmaCompactSpace X
d : ℕ
f : X → Y
U : Set X
hf : LocallyLipschitz (U.restrict f)
s : Set X
hsu : s ⊆ U
hs : ↑μH[↑d] s = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
sorry
State after:
no goals