constructor
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ IsBump fun x => f (-x)
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)