Theorem: lipschitz_image_null_set_is_null_set (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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
⊢ ↑μH[d] (f '' s) = 0
Tactic:
have aux : μH[d] (f '' s) ≤ (K : ENNReal) ^ d * μH[d] s := hf.hausdorffMeasure_image_le hd
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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * ↑μH[d] s
⊢ ↑μ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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * ↑μH[d] s
⊢ ↑μH[d] (f '' s) = 0
Tactic:
rw [hs] at aux
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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * 0
⊢ ↑μ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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) ≤ ↑K ^ d * 0
⊢ ↑μH[d] (f '' s) = 0
Tactic:
simp only [mul_zero, nonpos_iff_eq_zero, hs] at aux ⊢
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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) = 0
⊢ ↑μ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
d : ℝ
hd : d ≥ 0
s : Set X
f : X → Y
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : ↑μH[d] s = 0
aux : ↑μH[d] (f '' s) = 0
⊢ ↑μH[d] (f '' s) = 0
Tactic:
exact aux
State after:
no goals