ι : Type ?u.2206531
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(ofReal (abs a⁻¹) • volume) s = ofReal (abs a⁻¹) * ↑↑volume s
ι : Type ?u.2206531
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(Measure.map (fun x => a * x) volume) s = ofReal (abs a⁻¹) * ↑↑volume s
rw [map_volume_mul_left h]
no goals
ι : Type ?u.2206531
inst✝ : Fintype ι
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ ↑↑(ofReal (abs a⁻¹) • volume) s = ofReal (abs a⁻¹) * ↑↑volume s
rfl