exact HasCompactSupport.comp_homeomorph hf.left _
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f ((Homeomorph.neg α) x)
no goals