Theorem: Bump₁.absNthDeriv_bddAbove_image (ForML/BumpTopology.lean)

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ BddAbove (absNthDeriv n f '' K)
Tactic:
apply IsCompact.bddAbove_image hK
State after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ContinuousOn (absNthDeriv n f) K

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ContinuousOn (absNthDeriv n f) K
Tactic:
exact Continuous.continuousOn absNthDeriv_continuous
State after:
no goals