Theorem: C1_preserves_null_sets_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
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : SigmaCompactSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
d : ℕ
s : Set E
hsU : s ⊆ U
hs : ↑μH[↑d] s = 0
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
have : Convex ℝ U := sorry
State after:
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
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : SigmaCompactSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
d : ℕ
s : Set E
hsU : s ⊆ U
hs : ↑μH[↑d] s = 0
this : Convex ℝ U
⊢ ↑μH[↑d] (f '' s) = 0

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
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : SigmaCompactSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
d : ℕ
s : Set E
hsU : s ⊆ U
hs : ↑μH[↑d] s = 0
this : Convex ℝ U
⊢ ↑μH[↑d] (f '' s) = 0
Tactic:
exact locally_lipschitz_image_of_null_set_is_null_set_open
  (LocallyLipschitz.of_C1_on_open hU this hf) hsU hs
State after:
no goals