E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1956140
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
s : Set E
⊢ ↑↑μ ((fun a => ↑(AffineMap.homothety x r) a) '' s) = ↑↑μ ((fun x_1 => r • (x_1 - x) + x) '' s)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1956140
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
s : Set E
⊢ ↑↑μ (↑(AffineMap.homothety x r) '' s) = ↑↑μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s))
simp only [← image_smul, image_image, ← sub_eq_add_neg]
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1956140
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
s : Set E
⊢ ↑↑μ ((fun a => ↑(AffineMap.homothety x r) a) '' s) = ↑↑μ ((fun x_1 => r • (x_1 - x) + x) '' s)
rfl
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1956140
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ : Set E
x : E
r : ℝ
s : Set E
⊢ ↑↑μ ((fun y => y + x) '' (r • (fun y => y + -x) '' s)) = ENNReal.ofReal (abs (r ^ finrank ℝ E)) * ↑↑μ s
simp only [image_add_right, measure_preimage_add_right, add_haar_smul]