Theorem: IsBump.differentiable (ForML/Bump.lean)

State before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ 1 ≤ ⊤
Tactic:
norm_num
State after:
no goals